∀ {ι : Type u_1} (H : ι → Type u_3) [inst : (i : ι) → TopologicalSpace (H i)] (M : ι → Type u_2)
  [inst_1 : (i : ι) → TopologicalSpace (M i)] [inst_2 : (i : ι) → ChartedSpace (H i) (M i)] (f : (i : ι) → M i),
  ∀ i ∈ Set.univ, f i ∈ (chartAt (H i) (f i)).source