no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁' e₂').toLocalEquiv.source
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ e₂']