no goals
ι : Type u_2
α : ι → Type u_1
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((pi univ fun i => Ioc (x i) (update y i₀ m i)) ∪ pi univ fun i => Ioc (update x i₀ m i) (y i)) =
    pi univ fun i => Ioc (x i) (y i)
simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
  ← setOf_or, le_or_lt, setOf_true, univ_inter]