-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.param_eq
    {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (h : G.IsSRGWith n k ℓ μ) (hn : 0 < n) :
    k * (k - ℓ - 1) = (n - k - 1) * μ

Proof state:
case intro.convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ

Tactic:
intro w hw

Result:
case intro.convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ Gᶜ.neighborFinset v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Proof state:
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ G.Adj w v ∧ v ∉ G.neighborFinset v

Tactic:
exact ⟨hw.symm, G.not_mem_neighborFinset_self v⟩

Result:
no goals

Proof state:
case h.e'_3.h.e'_5
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ n - k - 1 = #(Gᶜ.neighborFinset v)

Tactic:
simp [h.compl.regular v]

Result:
no goals

Proof state:
case intro.convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) = k

Tactic:
simp [h.regular w]

Result:
no goals

Proof state:
case intro.convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset

Tactic:
congr!

Result:
no goals

Proof state:
case intro.convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ Gᶜ.neighborFinset v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Tactic:
simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset,
  ← Ne.eq_def] at hw

Result:
case intro.convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Proof state:
case intro.convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1

Tactic:
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⟩

Result:
case intro.convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1

Proof state:
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
this : DecidableEq V := Classical.decEq V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Tactic:
rw [← h.card, Fintype.card_pos_iff] at hn

Result:
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : Nonempty V
this : DecidableEq V := Classical.decEq V
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Proof state:
case intro.convert_3
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1

Tactic:
congr

Result:
case intro.convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w) = k

case intro.convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ

Proof state:
case h.e'_2.h.e'_5
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ k = #(G.neighborFinset v)

Tactic:
simp [h.regular v]

Result:
no goals