-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.card_commonNeighbors_eq_of_adj_compl (h : G.IsSRGWith n k ℓ μ) {v w : V}
    (ha : Gᶜ.Adj v w) : Fintype.card (Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Tactic:
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
  Set.toFinset_diff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
rw [compl_adj] at ha

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
have hne : v ≠ w := ne_of_adj _ ha

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - (1 + 1) = n - (2 * k - μ) - 2

Tactic:
rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2

Tactic:
simp_rw [compl_neighborFinset_sdiff_inter_eq]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
intro u

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ u ∈ {w} ∪ {v} → u ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ u ∈ {w} ∪ {v} → u ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬G.Adj v u ∧ ¬G.Adj w u

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

Tactic:
simp only [hne.symm, not_false_iff, mem_singleton]

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
⊢ u = w ∨ u = v → ¬G.Adj v u ∧ ¬G.Adj w u

Tactic:
rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
rw [card_sdiff, ← insert_eq, card_insert_of_not_mem, card_singleton, ← Finset.compl_union]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - (1 + 1) = n - (2 * k - μ) - 2

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ