α : Type ?u.205125
β : Type ?u.205128
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (↑(Fin.castLE (_ : ↑x ≤ m)) j) = 0
α : Type ?u.205125
β : Type ?u.205128
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(↑finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j : Fin ↑i, n (↑(Fin.castLE (_ : ↑i ≤ m)) j)
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
α : Type ?u.205125
β : Type ?u.205128
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (↑(Fin.castLE (_ : ↑x ≤ m)) j) = 0
α : Type ?u.205125
β : Type ?u.205128
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (↑(Fin.castLE (_ : ↑x ≤ m)) j) = 0
rintro x hx
no goals
α : Type ?u.205125
β : Type ?u.205128
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (↑(Fin.castLE (_ : ↑x ≤ m)) j) = 0
rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]