∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] {x y : M'},
  ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y