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
ha : Adj (Gᶜ) v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - μ) - 2
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
ha : Adj (Gᶜ) v w
⊢ Fintype.card ↑(commonNeighbors (Gᶜ) v w) = n - (2 * k - μ) - 2
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
ha : Adj (Gᶜ) v w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
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
ha : Adj (Gᶜ) v w
⊢ Finset.card (neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w})) = n - (2 * k - μ) - 2
simp_rw [compl_neighborFinset_sdiff_inter_eq]
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
ha : Adj (Gᶜ) v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
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
ha : Adj (Gᶜ) v w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
have hne : v ≠ w := ne_of_adj _ ha
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
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
ha : Adj (Gᶜ) v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
rw [compl_adj] at ha
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G v ∪ neighborFinset G w)ᶜ) - (1 + 1) = n - (2 * k - μ) - 2

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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ ¬w ∈ {v}

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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
rw [card_sdiff, ← insert_eq, card_insert_of_not_mem, card_singleton, ← Finset.compl_union]
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ Finset.card ((neighborFinset G v ∪ neighborFinset G w)ᶜ) - (1 + 1) = n - (2 * k - μ) - 2
rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ ¬w ∈ {v}
simp only [hne.symm, not_false_iff, mem_singleton]
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u ∈ {w} ∪ {v} → u ∈ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
intro u
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬Adj G v u ∧ ¬Adj G w u
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u ∈ {w} ∪ {v} → u ∈ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
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
ha : v ≠ w ∧ ¬Adj G v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬Adj G v u ∧ ¬Adj G w u
rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2