[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ ¬Adj ⊥ v w → Fintype.card ↑(commonNeighbors ⊥ v w) = 0
[PROOFSTEP]
simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
⊢ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (fun x => x ∈ commonNeighbors ⊥ v w) univ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp [mem_commonNeighbors]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ Fintype.card ↑(commonNeighbors ⊤ v w) = Fintype.card V - 2
[PROOFSTEP]
rw [card_commonNeighbors_top]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj ⊤ v w
⊢ v ≠ w
[PROOFSTEP]
exact h
[GOAL]
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)
[PROOFSTEP]
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
[GOAL]
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)
[PROOFSTEP]
rw [Nat.sub_add_cancel, ← Set.toFinset_card]
  -- porting note: Set.toFinset_inter needs workaround to use unification to solve for one of the
    -- instance arguments:
[GOAL]
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
[PROOFSTEP]
simp [commonNeighbors, @Set.toFinset_inter _ _ _ _ _ _ (_), ← neighborFinset_def, Finset.card_union_add_card_inter,
  card_neighborFinset_eq_degree, h.regular.degree_eq, two_mul]
[GOAL]
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
[PROOFSTEP]
apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
[GOAL]
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
[PROOFSTEP]
simp [h.regular.degree_eq, two_mul]
[GOAL]
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 ℓ μ
hne : v ≠ w
ha : ¬Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - μ
[PROOFSTEP]
rw [← h.of_not_adj v w hne ha]
[GOAL]
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 ℓ μ
hne : v ≠ w
ha : ¬Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
apply h.card_neighborFinset_union_eq
[GOAL]
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 ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - ℓ
[PROOFSTEP]
rw [← h.of_adj v w ha]
[GOAL]
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 ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
[PROOFSTEP]
apply h.card_neighborFinset_union_eq
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
⊢ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) =
    ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ a✝ ∈ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) ↔
    a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ ¬a✝ ∈ (neighborFinset G v)ᶜ \ {v} ∩ ((neighborFinset G w)ᶜ \ {w}) ↔
    ¬a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v})
[PROOFSTEP]
simp [imp_iff_not_or, or_assoc, or_comm, or_left_comm]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
⊢ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v}) = (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ a✝ ∈ ((neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ) \ ({w} ∪ {v}) ↔
    a✝ ∈ (neighborFinset G v)ᶜ ∩ (neighborFinset G w)ᶜ
[PROOFSTEP]
simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp, mem_neighborFinset, mem_inter, mem_singleton]
[GOAL]
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ ¬Adj G v a✝ → ¬Adj G w a✝ → ¬(a✝ = w ∨ a✝ = v)
[PROOFSTEP]
rintro hnv hnw (rfl | rfl)
[GOAL]
case a.inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v a✝ : V
hnv : ¬Adj G v a✝
h : Adj G v a✝
hnw : ¬Adj G a✝ a✝
⊢ False
[PROOFSTEP]
exact hnv h
[GOAL]
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ False
[PROOFSTEP]
apply hnw
[GOAL]
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ Adj G w a✝
[PROOFSTEP]
rwa [adj_comm]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree Gᶜ (n - k - 1)
[PROOFSTEP]
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree Gᶜ (Fintype.card V - 1 - k)
[PROOFSTEP]
exact h.regular.compl
[GOAL]
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
[PROOFSTEP]
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
  Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
[GOAL]
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
[PROOFSTEP]
simp_rw [compl_neighborFinset_sdiff_inter_eq]
[GOAL]
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
[PROOFSTEP]
have hne : v ≠ w := ne_of_adj _ ha
[GOAL]
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
[PROOFSTEP]
rw [compl_adj] at ha 
[GOAL]
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
[PROOFSTEP]
rw [card_sdiff, ← insert_eq, card_insert_of_not_mem, card_singleton, ← Finset.compl_union]
[GOAL]
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
[PROOFSTEP]
rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
[GOAL]
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}
[PROOFSTEP]
simp only [hne.symm, not_false_iff, mem_singleton]
[GOAL]
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)ᶜ
[PROOFSTEP]
intro u
[GOAL]
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)ᶜ
[PROOFSTEP]
simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
[GOAL]
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
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬Adj G v u
hne : v ≠ u
⊢ ¬Adj G v u ∧ ¬Adj G u u
[PROOFSTEP]
simpa [adj_comm] using ha.2
[GOAL]
case inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬Adj G u w
hne : u ≠ w
⊢ ¬Adj G u u ∧ ¬Adj G w u
[PROOFSTEP]
simpa [adj_comm] using ha.2
[GOAL]
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 - ℓ)
[PROOFSTEP]
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
  Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
[GOAL]
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 - ℓ)
[PROOFSTEP]
simp only [not_and, Classical.not_not, compl_adj] at hna 
[GOAL]
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 - ℓ)
[PROOFSTEP]
have h2' := hna hn
[GOAL]
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 - ℓ)
[PROOFSTEP]
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']
[GOAL]
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 - ℓ)
[PROOFSTEP]
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
hn : 0 < n
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
rw [← h.card, Fintype.card_pos_iff] at hn 
[GOAL]
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
hn : Nonempty V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
obtain ⟨v⟩ := hn
[GOAL]
case intro
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ
[PROOFSTEP]
convert card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
[GOAL]
case h.e'_2.h.e'_5
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ k = Finset.card (neighborFinset G v)
[PROOFSTEP]
simp [h.regular v]
[GOAL]
case h.e'_3.h.e'_5
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ n - k - 1 = Finset.card (neighborFinset Gᶜ v)
[PROOFSTEP]
simp [h.compl.regular v]
[GOAL]
case intro.convert_3
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ ∀ (a : V), a ∈ neighborFinset G v → Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) a) = k - ℓ - 1
[PROOFSTEP]
intro w hw
[GOAL]
case intro.convert_3
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
hw : w ∈ neighborFinset G v
⊢ Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) w) = k - ℓ - 1
[PROOFSTEP]
rw [mem_neighborFinset] at hw 
[GOAL]
case intro.convert_3
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
hw : Adj G v w
⊢ Finset.card (bipartiteAbove G.Adj (neighborFinset Gᶜ v) w) = k - ℓ - 1
[PROOFSTEP]
simp_rw [bipartiteAbove, show G.Adj w = fun a => G.Adj w a by rfl, ← mem_neighborFinset, filter_mem_eq_inter]
[GOAL]
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
hw : Adj G v w
⊢ Adj G w = fun a => Adj G w a
[PROOFSTEP]
rfl
[GOAL]
case intro.convert_3
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
hw : Adj G v w
⊢ Finset.card (neighborFinset Gᶜ v ∩ neighborFinset G w) = k - ℓ - 1
[PROOFSTEP]
have s : { v } ⊆ G.neighborFinset w \ G.neighborFinset v :=
  by
  rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
  exact ⟨hw.symm, G.not_mem_neighborFinset_self v⟩
[GOAL]
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
hw : Adj G v w
⊢ {v} ⊆ neighborFinset G w \ neighborFinset G v
[PROOFSTEP]
rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
[GOAL]
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
hw : Adj G v w
⊢ Adj G w v ∧ ¬v ∈ neighborFinset G v
[PROOFSTEP]
exact ⟨hw.symm, G.not_mem_neighborFinset_self v⟩
[GOAL]
case intro.convert_3
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset Gᶜ v ∩ neighborFinset G w) = k - ℓ - 1
[PROOFSTEP]
rw [inter_comm, neighborFinset_compl, inter_sdiff, ← sdiff_eq_inter_compl, card_sdiff s, card_singleton, ←
  sdiff_inter_self_left, card_sdiff (by apply inter_subset_left)]
[GOAL]
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ neighborFinset G w ∩ neighborFinset G v ⊆ neighborFinset G w
[PROOFSTEP]
apply inter_subset_left
[GOAL]
case intro.convert_3
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w) - Finset.card (neighborFinset G w ∩ neighborFinset G v) - 1 = k - ℓ - 1
[PROOFSTEP]
congr
[GOAL]
case intro.convert_3.e_a.e_a
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w) = k
[PROOFSTEP]
simp [h.regular w]
[GOAL]
case intro.convert_3.e_a.e_a
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (neighborFinset G w ∩ neighborFinset G v) = ℓ
[PROOFSTEP]
simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw, ← Set.toFinset_card]
[GOAL]
case intro.convert_3.e_a.e_a
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
hw : Adj G v w
s : {v} ⊆ neighborFinset G w \ neighborFinset G v
⊢ Finset.card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) = Finset.card (Set.toFinset (commonNeighbors G v w))
[PROOFSTEP]
congr!
[GOAL]
case intro.convert_4
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
v : V
⊢ ∀ (b : V), b ∈ neighborFinset Gᶜ v → Finset.card (bipartiteBelow G.Adj (neighborFinset G v) b) = μ
[PROOFSTEP]
intro w hw
[GOAL]
case intro.convert_4
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
hw : w ∈ neighborFinset Gᶜ v
⊢ Finset.card (bipartiteBelow G.Adj (neighborFinset G v) w) = μ
[PROOFSTEP]
simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset, ← Ne.def] at hw 
[GOAL]
case intro.convert_4
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
hw : ¬Adj G v w ∧ w ≠ v
⊢ Finset.card (bipartiteBelow G.Adj (neighborFinset G v) w) = μ
[PROOFSTEP]
simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter, neighborFinset_def, ← Set.toFinset_inter,
  ← h.of_not_adj v w hw.2.symm hw.1, ← Set.toFinset_card]
[GOAL]
case intro.convert_4
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
hw : ¬Adj G v w ∧ w ≠ v
⊢ Finset.card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) = Finset.card (Set.toFinset (commonNeighbors G v w))
[PROOFSTEP]
congr!
[GOAL]
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
⊢ adjMatrix α G ^ 2 = k • 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ
[PROOFSTEP]
ext v w
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ (adjMatrix α G ^ 2) v w = (k • 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
[PROOFSTEP]
simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply, adjMatrix_apply,
  compl_adj]
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ ↑(Fintype.card { x // Walk.length x = 2 }) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
rw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
[GOAL]
case a.h
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
obtain rfl | hn := eq_or_ne v w
[GOAL]
case a.h.inl
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v : V
⊢ ↑(Fintype.card ↑(commonNeighbors G v v)) =
    (k • OfNat.ofNat 1 v v + ℓ • if Adj G v v then 1 else 0) + μ • if v ≠ v ∧ ¬Adj G v v then 1 else 0
[PROOFSTEP]
rw [← Set.toFinset_card]
[GOAL]
case a.h.inl
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v : V
⊢ ↑(Finset.card (Set.toFinset (commonNeighbors G v v))) =
    (k • OfNat.ofNat 1 v v + ℓ • if Adj G v v then 1 else 0) + μ • if v ≠ v ∧ ¬Adj G v v then 1 else 0
[PROOFSTEP]
simp [commonNeighbors, ← neighborFinset_def, h.regular v]
[GOAL]
case a.h.inr
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • OfNat.ofNat 1 v w + ℓ • if Adj G v w then 1 else 0) + μ • if v ≠ w ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]
[GOAL]
case a.h.inr
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
by_cases ha : G.Adj v w
[GOAL]
case pos
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one]
[GOAL]
case neg
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) =
    (k • 0 + ℓ • if Adj G v w then 1 else 0) + μ • if True ∧ ¬Adj G v w then 1 else 0
[PROOFSTEP]
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one]
[GOAL]
case pos
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) = ↑ℓ
[PROOFSTEP]
rw [h.of_adj v w ha]
[GOAL]
case neg
V : Type u
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
α : Type u_1
inst✝ : Semiring α
h : IsSRGWith G n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬Adj G v w
⊢ ↑(Fintype.card ↑(commonNeighbors G v w)) = ↑μ
[PROOFSTEP]
rw [h.of_not_adj v w hn ha]
