α : Type ?u.74019
β : Type ?u.74022
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (↑(natAdd a) j) = 1
⊢ ∏ i : Fin a, f (↑(castAdd b) i) = ∏ i : Fin a, f (↑(castLE (_ : a ≤ a + b)) i)
α : Type ?u.74019
β : Type ?u.74022
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (↑(natAdd a) j) = 1
⊢ ∏ i : Fin (a + b), f i = ∏ i : Fin a, f (↑(castLE (_ : a ≤ a + b)) i)
rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
no goals
α : Type ?u.74019
β : Type ?u.74022
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (↑(natAdd a) j) = 1
⊢ ∏ i : Fin a, f (↑(castAdd b) i) = ∏ i : Fin a, f (↑(castLE (_ : a ≤ a + b)) i)
rfl