gistfile1.txt

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,
  { simp },
  { simp },
  { ext y,
    rcases y with ⟨a, b⟩,
    simp [local_equiv.trans_source],
    tauto }
end