V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Fintype.card ↑(commonNeighbors G v w) =
    2 * k - Fintype.card ↑(commonNeighbors G v w) + Fintype.card ↑(commonNeighbors G v w)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Finset.card (Set.toFinset (commonNeighbors G v w)) = 2 * k

V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ 2 * k
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Fintype.card ↑(commonNeighbors G v w) =
    2 * k - Fintype.card ↑(commonNeighbors G v w) + Fintype.card ↑(commonNeighbors G v w)
rw [Nat.sub_add_cancel, ← Set.toFinset_card]
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) + Finset.card (Set.toFinset (commonNeighbors G v w)) = 2 * k
simp [commonNeighbors, @Set.toFinset_inter _ _ _ _ _ _ (_),
  ← neighborFinset_def, Finset.card_union_add_card_inter, card_neighborFinset_eq_degree,
  h.regular.degree_eq, two_mul]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ degree G v ≤ 2 * k
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ 2 * k
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
⊢ degree G v ≤ 2 * k
simp [h.regular.degree_eq, two_mul]