awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
rw : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
rw₁ : Fintype.card V - (2 * k - μ) - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2
rw₂ rw₃ : Fintype.card V - (2 * k - μ) - HAdd.hAdd (α := ℕ) 1 1 = Fintype.card V - (2 * k - μ) - 2
⊢ #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ - HAdd.hAdd (α := ℕ) 1 1 = n - (2 * k - μ) - 2

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

Premises used: Finset.card_compl, SimpleGraph.IsSRGWith.card, SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : 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]

Premises used: Finset.mem_singleton, Ne.symm, not_false_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
u : V
simp : u = w ∨ u = v → ¬G.Adj v u ∧ ¬G.Adj w u
⊢ Membership.mem (γ := Finset V) ({w} ∪ {v}) u → u ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

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

Premises used: Finset.mem_singleton, Finset.mem_compl, SimpleGraph.mem_neighborFinset, Finset.mem_union, Finset.mem_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v u : V
ha : v ≠ u ∧ ¬G.Adj v u
hne : v ≠ u
⊢ ¬G.Adj v u ∧ ¬G.Adj u u

Tactic:
simpa [adj_comm] using ha.2

Premises used: And.right, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
w u : V
ha : u ≠ w ∧ ¬G.Adj u w
hne : u ≠ w
⊢ ¬G.Adj u u ∧ ¬G.Adj w u

Tactic:
simpa [adj_comm] using ha.2

Premises used: And.right, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
simp : #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
⊢ Fintype.card.{u} (↑(Gᶜ.commonNeighbors v w) : Type u) = n - (2 * k - ℓ)

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

Premises used: Set.toFinset_compl, Set.toFinset_diff, SimpleGraph.neighborSet_compl, SimpleGraph.commonNeighbors, Set.toFinset_card, Set.toFinset_singleton, Set.toFinset_inter, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ v ≠ w → G.Adj v w

Tactic:
simp only [not_and, Classical.not_not, compl_adj] at hna

Premises used: Classical.not_not, SimpleGraph.compl_adj, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
⊢ G.Adj v w

Tactic:
have h2' := hna hn
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
simp_rw : #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)

Tactic:
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']

Premises used: SimpleGraph.sdiff_compl_neighborFinset_inter_eq, SimpleGraph.compl_neighborFinset_sdiff_inter_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
rwa : #(G.neighborFinset v ∪ G.neighborFinset w)ᶜ = n - (2 * k - ℓ)
rwa₁ : Fintype.card V - #(G.neighborFinset v ∪ G.neighborFinset w) = n - (2 * k - ℓ)
rwa₂ : Fintype.card V - (2 * k - ℓ) = n - (2 * k - ℓ)
rwa₃ : G.Adj v w
rwa₄ : Fintype.card V - (2 * k - ℓ) = Fintype.card V - (2 * k - ℓ)
rwa₅ : G.Adj v w
rwa₆ : Fintype.card V - (2 * k - ℓ) = Fintype.card V - (2 * k - ℓ)
rwa₇ rwa₈ rwa₉ : G.Adj v w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) = n - (2 * k - ℓ)

Tactic:
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]

Premises used: Finset.compl_union, Finset.card_compl, SimpleGraph.IsSRGWith.card, SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
this : DecidableEq V := Classical.decEq V
⊢ Nonempty V

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

Premises used: SimpleGraph.IsSRGWith.card, Fintype.card_pos_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : Nonempty V
this : DecidableEq V := Classical.decEq V
obtain : ∀ (v : V), k * (k - ℓ - 1) = (n - k - 1) * μ
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Tactic:
obtain ⟨v⟩ := hn
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ #(G.neighborFinset v) * (k - ℓ - 1) = #(Gᶜ.neighborFinset v) * μ

Tactic:
card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _

Premises used: SimpleGraph.Adj, Finset.card_mul_eq_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
h₁ : k = #(G.neighborFinset v)
h₂ : n - k - 1 = #(Gᶜ.neighborFinset v)
convert_3 : ∀ a ∈ G.neighborFinset v, #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) a) = k - ℓ - 1
convert_4 : ∀ b ∈ Gᶜ.neighborFinset v, #(bipartiteBelow G.Adj (G.neighborFinset v) b) = μ
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Tactic:
convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _

Premises used: SimpleGraph.Adj, Finset.card_mul_eq_card_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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]

Premises used: SimpleGraph.IsSRGWith.regular
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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]

Premises used: SimpleGraph.IsSRGWith.regular, SimpleGraph.IsSRGWith.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ G.neighborFinset v
⊢ G.Adj v w

Tactic:
rw [mem_neighborFinset] at hw

Premises used: SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
convert_3 : #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1
⊢ #(bipartiteAbove G.Adj (Gᶜ.neighborFinset v) w) = k - ℓ - 1

Tactic:
simp_rw [bipartiteAbove, ← mem_neighborFinset, filter_mem_eq_inter]

Premises used: Finset.bipartiteAbove, SimpleGraph.mem_neighborFinset, Finset.filter_mem_eq_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
rw : G.Adj w v ∧ v ∉ G.neighborFinset v
⊢ {v} ⊆ G.neighborFinset w \ G.neighborFinset v

Tactic:
rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]

Premises used: Finset.singleton_subset_iff, Finset.mem_sdiff, SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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:
⟨hw.symm, G.notMem_neighborFinset_self v⟩

Premises used: SimpleGraph.Adj.symm, SimpleGraph.notMem_neighborFinset_self, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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.notMem_neighborFinset_self v⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
⊢ {v} ⊆ G.neighborFinset w \ G.neighborFinset v

Tactic:
have s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v := by
      rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
      exact ⟨hw.symm, G.notMem_neighborFinset_self v⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
convert_3 : #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1
⊢ #(Gᶜ.neighborFinset v ∩ G.neighborFinset w) = k - ℓ - 1

Tactic:
rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl,
      card_sdiff_of_subset s, card_singleton, ← sdiff_inter_self_left,
      card_sdiff_of_subset inter_subset_left]

Premises used: Finset.inter_sdiff_assoc, Finset.card_sdiff_of_subset, SimpleGraph.neighborFinset_compl, Finset.inter_comm, Finset.sdiff_inter_self_left, Finset.inter_subset_left, Finset.sdiff_eq_inter_compl, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
convert_3 : #(G.neighborFinset w) = k
convert_3₁ : #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ
⊢ #(G.neighborFinset w) - #(G.neighborFinset w ∩ G.neighborFinset v) - 1 = k - ℓ - 1

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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]

Premises used: SimpleGraph.IsSRGWith.regular
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
convert_3 : #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
⊢ #(G.neighborFinset w ∩ G.neighborFinset v) = ℓ

Tactic:
simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw,
        ← Set.toFinset_card]

Premises used: Finset.inter_comm, Set.toFinset_card, Set.toFinset_inter, SimpleGraph.IsSRGWith.of_adj, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : 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!
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∈ Gᶜ.neighborFinset v
⊢ ¬G.Adj v w ∧ w ≠ v

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

Premises used: Finset.mem_singleton, SimpleGraph.neighborFinset_compl, Ne.eq_def, Finset.mem_compl, Finset.mem_sdiff, SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
convert_4 : #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Tactic:
simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter,
      neighborFinset_def, ← Set.toFinset_inter, ← h.of_not_adj hw.2.symm hw.1,
      ← Set.toFinset_card]

Premises used: Ne.symm, Set.toFinset_card, Set.toFinset_inter, SimpleGraph.mem_neighborFinset, And.right, And.left, Finset.bipartiteBelow, SimpleGraph.IsSRGWith.of_not_adj, Finset.filter_mem_eq_inter, SimpleGraph.neighborFinset_def, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
n k ℓ μ : ℕ
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(G.neighborSet v ∩ G.neighborSet w).toFinset = #(G.commonNeighbors v w).toFinset

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
a :
  ∀ (v w : V),
    HPow.hPow (β := ℕ) (adjMatrix α G) 2 v w =
      (HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 2 = HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
a :
  (↑(Fintype.card.{u} (↑{p : G.Walk v w | p.length = 2} : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
⊢ HPow.hPow (β := ℕ) (adjMatrix α G) 2 v w =
    (HSMul.hSMul (β := Matrix V V α) k 1 + ℓ • adjMatrix α G + μ • adjMatrix α Gᶜ) v w

Tactic:
simp only [adjMatrix_pow_apply_eq_card_walk, Matrix.add_apply, Matrix.smul_apply,
    adjMatrix_apply, compl_adj]

Premises used: SimpleGraph.adjMatrix_apply, Matrix.add_apply, Matrix.smul_apply, SimpleGraph.adjMatrix_pow_apply_eq_card_walk, SimpleGraph.compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
a :
  (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)
⊢ (↑(Fintype.card.{u} (↑{p : G.Walk v w | p.length = 2} : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)

Tactic:
rw [@Fintype.card_congr _ _ (G.fintypeSetWalkLength v w 2) _
    (G.walkLengthTwoEquivCommonNeighbors v w)]

Premises used: Fintype.card_congr, SimpleGraph.walkLengthTwoEquivCommonNeighbors
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
a :
  (↑(#(G.commonNeighbors v v).toFinset) : α) =
    HSMul.hSMul (β := α) k (1 v v) + HSMul.hSMul (β := α) ℓ (if G.Adj v v then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ v ∧ ¬G.Adj v v then 1 else 0)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v v) : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v v) + HSMul.hSMul (β := α) ℓ (if G.Adj v v then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ v ∧ ¬G.Adj v v then 1 else 0)

Tactic:
rw [← Set.toFinset_card]

Premises used: Set.toFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ (↑(#(G.commonNeighbors v v).toFinset) : α) =
    HSMul.hSMul (β := α) k (1 v v) + HSMul.hSMul (β := α) ℓ (if G.Adj v v then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ v ∧ ¬G.Adj v v then 1 else 0)

Tactic:
simp [commonNeighbors, ← neighborFinset_def, h.regular v]

Premises used: SimpleGraph.commonNeighbors, SimpleGraph.IsSRGWith.regular, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
a :
  (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k (1 v w) + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if v ≠ w ∧ ¬G.Adj v w then 1 else 0)

Tactic:
simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]

Premises used: Ne.symm, ne_eq, Matrix.one_apply_ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
pos :
  ∀ (ha : G.Adj v w),
    (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
      HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
        HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
neg :
  ∀ (ha : ¬G.Adj v w),
    (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
      HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
        HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)

Tactic:
by_cases ha : G.Adj v w

Premises used: SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
pos : Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑ℓ : α)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)

Tactic:
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]

Premises used: and_self, ite_false, smul_zero, not_true_eq_false, ite_true, zero_add, nsmul_eq_mul, and_false, mul_one, add_zero, not_false_eq_true
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
neg : Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑μ : α)
⊢ (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) =
    HSMul.hSMul (β := α) k 0 + HSMul.hSMul (β := α) ℓ (if G.Adj v w then 1 else 0) +
      HSMul.hSMul (β := α) μ (if ¬False ∧ ¬G.Adj v w then 1 else 0)

Tactic:
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one,
        not_true_eq_false, not_false_eq_true, and_false, and_self]

Premises used: and_self, ite_false, smul_zero, not_true_eq_false, ite_true, zero_add, nsmul_eq_mul, and_false, mul_one, add_zero, not_false_eq_true
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : G.Adj v w
pos pos₁ : Eq.{u_1 + 1} (α := α) (↑ℓ : α) (↑ℓ : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑ℓ : α)

Tactic:
rw [h.of_adj v w ha]

Premises used: SimpleGraph.IsSRGWith.of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n k ℓ μ : ℕ
inst_2 : DecidableEq V
α : Type u_1
inst_3 : Semiring α
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
ha : ¬G.Adj v w
neg neg₁ : Eq.{u_1 + 1} (α := α) (↑μ : α) (↑μ : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(Fintype.card.{u} (↑(G.commonNeighbors v w) : Type u)) : α) (↑μ : α)

Tactic:
rw [h.of_not_adj hn ha]

Premises used: SimpleGraph.IsSRGWith.of_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
v_1 w_1 : V
h : s(v, w) = s(v_1, w_1)
rw : s(v, w) ∈ G.edgeSet
⊢ G.Adj v_1 w_1

Tactic:
rw [← G.mem_edgeSet, ← h]

Premises used: SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
v_1 w_1 : V
h : s(v, w) = s(v_1, w_1)
⊢ s(v, w) ∈ G.edgeSet

Tactic:
hvw

Premises used: Set.Mem, setOf, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
v w : V
hvw : G.Adj v w
v_1 w_1 : V
h : s(v, w) = s(v_1, w_1)
⊢ s(v, w) ∈ G.edgeSet

Tactic:
exact hvw