ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (pi univ fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i => Ioc (x i) (y i)
ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ (pi univ fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i => Ioc (x i) (y i)
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
    inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi ({i₀}ᶜ) fun j => Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ pi ({i₀}ᶜ) fun j => Ioc (x j) (y j)
ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (pi univ fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i => Ioc (x i) (y i)
simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
  singleton_pi', ← inter_assoc, this]
no goals
ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi ({i₀}ᶜ) fun j => Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ pi ({i₀}ᶜ) fun j => Ioc (x j) (y j)
rfl
no goals
ι : Type u_2
α : ι → Type u_1
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
  inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]