chore(Combinatorics/SimpleGraph/Finite): fix Fintype instances in edgeFinset_inf (leanprover-community#41789)

Unlike `edgeFinset_sup`, `edgeFinset_inf` only accepts `Fintype` instances for `G` and `H` and not their inf, relying on the [`fintypeEdgeSetInf`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Basic.html#SimpleGraph.fintypeEdgeSetInf) instance providing it.
This means the theorem can't be used with a different `Fintype (G₁ ⊓ G₂).edgeSet`.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -99,7 +99,8 @@ theorem edgeFinset_sup [Fintype (edgeSet (G₁ ⊔ G₂))] [DecidableEq V] :
     (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset := by simp [edgeFinset]
 
 @[simp]
-theorem edgeFinset_inf [DecidableEq V] : (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset := by
+theorem edgeFinset_inf [Fintype (G₁ ⊓ G₂).edgeSet] [DecidableEq V] :
+    (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset := by
   simp [edgeFinset]
 
 @[simp]