no goals
α : Type u
β : Type v
γ : Type ?u.533113
δ : Type ?u.533116
ε : Type ?u.533119
ζ : Type ?u.533122
ι : Type u_1
κ : Type u_2
σ : ι → Type u_3
τ : κ → Type u_4
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h₁ : Injective f₁
⊢ Inducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Inducing (f₂ i)
simp only [inducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk, ← map_sigma_mk_comap h₁,
  map_inj sigma_mk_injective]