[Merged by Bors] - feat: Port Combinatorics.SimpleGraph.StronglyRegular

[casavaca]

---

• depends on: [Merged by Bors] - feat: Port Combinatorics.SimpleGraph.Basic #1883

Help wanted: One error left: This simp doesn't work. It's weird because if you guide lean, rw doesn't work, even if it looks the same. I guess it has something to do with Quot.liftOn which hide behind dsimp [Finset.card, Multiset.card]?

theorem h : card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) = k := sorry
example : Fintype.card (G.commonNeighbors v w) = k := by
  rw [←Set.toFinset_card]
  unfold commonNeighbors
  have hh := @h V _ G _ k v w
  rw [←hh] --- Here 1
  congr    --- Here 2
  simp [Set.fintypeInterOfRight]

at Here 1: look the same but it's not.

⊢ card (Set.toFinset (neighborSet G v ∩ neighborSet G w)) =
  card (Set.toFinset (neighborSet G v ∩ neighborSet G w))

at Here 2:

⊢ (Subtype.fintype fun x => x ∈ neighborSet G v ∩ neighborSet G w) =
    Set.fintypeInterOfRight (neighborSet G v) (neighborSet G w)

[semorrison]

This PR/issue depends on:

• [Merged by Bors] - feat: Port Combinatorics.SimpleGraph.Basic #1883
  By Dependent Issues (🤖). Happy coding!

[kmill]

@casavaca It basically comes down to how in Lean 3 there's a feature where typeclass arguments can be solved for using unification as a fallback, and we designed a number of lemmas with this feature in mind. One workaround is to use @ and (_) arguments (I've left a porting note).

[ChrisHughes24]

bors r+

[bors]

👎 Rejected by label

[ChrisHughes24]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style