α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x : Fin a ⊕ Fin b, f (Equiv.toFun finSumFinEquiv x) =
    (∏ i : Fin a, f (↑(castAdd b) i)) * ∏ i : Fin b, f (↑(natAdd a) i)

α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ i : Fin (a + b), f i = (∏ i : Fin a, f (↑(castAdd b) i)) * ∏ i : Fin b, f (↑(natAdd a) i)
rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
no goals
α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x : Fin a ⊕ Fin b, f (Equiv.toFun finSumFinEquiv x) =
    (∏ i : Fin a, f (↑(castAdd b) i)) * ∏ i : Fin b, f (↑(natAdd a) i)
apply Fintype.prod_sum_type
α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
intro x
no goals
α : Type ?u.65773
β : Type ?u.65776
M : Type u_1
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (Equiv.toFun finSumFinEquiv (↑finSumFinEquiv.symm x))
simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]