simp
case h
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x✝ : φ i
⊢ (comp (proj i) (single i)) x✝ = (id R (φ i)) x✝
no goals