Product over Fin d to product over range d

Stream: general

[Strategist _]

If you had a product (\prod) over elements of type Fin d, that should be equal to a product over elements in range d (as written in the example below). Is there some lemma or tactic that would allow you to swap them out for each other easily?

Thanks!

import Mathlib
import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fin.Basic

open Real
open Finset

variable {d : ℕ}

example (f : ℕ → ℝ) : ∏ i : Fin d, f i = ∏ i ∈ range d, f i := sorry

[Daniel Weber]

This is docs#Fin.prod_univ_eq_prod_range (I found it by trying by exact?)

[Strategist _]

Oh I didn't know about exact?. That's perfect, thank you so much!