V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Adj (Gᶜ) v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Adj (Gᶜ) v w
⊢ Fintype.card ↑(commonNeighbors (Gᶜ) v w) = n - (2 * k - ℓ)
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
  Set.toFinset_diff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Adj (Gᶜ) v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
simp only [not_and, Classical.not_not, compl_adj] at hna
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
have h2' := hna hn
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) = n - (2 * k - ℓ)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - ℓ)
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → Adj G v w
h2' : Adj G v w
⊢ Finset.card (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) = n - (2 * k - ℓ)
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]