no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.66912
ε : Type ?u.66915
ζ : Type ?u.66918
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
b : β
f : α → γ
⊢ (Inducing fun x => (f x, b)) ↔ Inducing f
simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp,
  induced_const, inf_top_eq]