no goals
α : Type u_1
β : Type ?u.51670
γ : Type ?u.51673
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n
simp
no goals
α : Type u_1
β : Type ?u.51670
γ : Type ?u.51673
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (i : Fin n), f ↑i = f ↑(↑(equivSubtype.trans (Equiv.subtypeEquivRight (_ : ∀ (a : ℕ), a < n ↔ a ∈ range n))) i)
simp
no goals
α : Type u_1
β : Type ?u.51670
γ : Type ?u.51673
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i : { x // x ∈ range n }, f ↑i = ∏ i in range n, f i
rw [← attach_eq_univ, prod_attach]