sgouezel

lemma prod_symm (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
  (e.prod e').symm = (e.symm.prod e'.symm) :=
by ext x : 1; simp

lemma prod_comp {η : Type*} {ε : Type*} [topological_space η] [topological_space ε]
  (e : local_homeomorph α β) (f : local_homeomorph β γ)
  (e' : local_homeomorph δ η) (f' : local_homeomorph η ε):
  (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
begin
  ext x : 1,

sgouezel

1 goal
𝕜 : Type u_1,
E : Type u_2,
F : Type u_3,
G : Type u_4,
_inst_1 : normed_group.{u_2} E,
_inst_2 : normed_group.{u_3} F,
_inst_3 : normed_group.{u_4} G,
_inst_4 : nondiscrete_normed_field.{u_1} 𝕜,
_inst_5 : @normed_space.{u_1 u_2} 𝕜 E (@nondiscrete_normed_field.to_normed_field.{u_1} 𝕜 _inst_4) _inst_1,