α : Type ?u.64969
β : Type ?u.64972
M : Type u_1
inst✝ : CommMonoid M
a : ℕ
f : Fin a → M
⊢ ∏ i : Fin a, f (↑(cast (_ : a = a)) i) = ∏ i : Fin a, f i
α : Type ?u.64969
β : Type ?u.64972
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
⊢ ∏ i : Fin a, f (↑(cast h) i) = ∏ i : Fin b, f i
subst h
no goals
α : Type ?u.64969
β : Type ?u.64972
M : Type u_1
inst✝ : CommMonoid M
a : ℕ
f : Fin a → M
⊢ ∏ i : Fin a, f (↑(cast (_ : a = a)) i) = ∏ i : Fin a, f i
congr