no goals
α : Type u_1
β : Type u_2
γ : Type ?u.63296
δ : Type ?u.63299
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ prod (LocalEquiv.refl α) (LocalEquiv.refl β) = LocalEquiv.refl (α × β)
ext ⟨x, y⟩ <;> simp