no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.67982
ζ : Type ?u.67985
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : _root_.Embedding f
hg : _root_.Embedding g
src✝ : Inducing (Prod.map f g) := Inducing.prod_map hf.toInducing hg.toInducing
x✝¹ x✝ : α × γ
x₁ : α
x₂ : γ
y₁ : α
y₂ : γ
⊢ Prod.map f g (x₁, x₂) = Prod.map f g (y₁, y₂) → (x₁, x₂) = (y₁, y₂)
simp [hf.inj.eq_iff, hg.inj.eq_iff]