[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Ici (x i)) ↔ y ∈ Ici x
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Iic (x i)) ↔ y ∈ Iic x
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Icc (x i) (y✝ i)) ↔ y ∈ Icc x y✝
[PROOFSTEP]
simp [Pi.le_def, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ (pi univ fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc, inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc, inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (pi univ fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({ i₀ } : Set ι), singleton_pi', ← inter_assoc,
  this]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
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)
[PROOFSTEP]
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)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
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₀)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm, inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
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)
[PROOFSTEP]
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]
[GOAL]
ι : Type u_1
α : ι → Type u_2
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)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ Disjoint (pi univ fun i => Ioc (x i) (update y i₀ m i)) (pi univ fun i => Ioc (update x i₀ m i) (y i))
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ ∀ ⦃a : (i : ι) → α i⦄,
    (a ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)) → ¬a ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
[PROOFSTEP]
rintro z h₁ h₂
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
⊢ False
[PROOFSTEP]
refine' (h₁ i₀ (mem_univ _)).2.not_lt _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
⊢ update y i₀ m i₀ < z i₀
[PROOFSTEP]
simpa only [Function.update_same] using (h₂ i₀ (mem_univ _)).1
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b = Icc (update f i a) (update f i b)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ Icc (update f i a) (update f i b)
[PROOFSTEP]
rw [← Set.pi_univ_Icc]
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
refine' ⟨_, fun h => ⟨x i, _, _⟩⟩
[GOAL]
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b → x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case h.refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b c : α i
hc : c ∈ Icc a b
⊢ update f i c ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
simpa [update_le_update_iff]
[GOAL]
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b
[PROOFSTEP]
simpa only [Function.update_same] using h i (mem_univ i)
[GOAL]
case h.refine'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x
[PROOFSTEP]
ext j
[GOAL]
case h.refine'_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
j : ι
⊢ update f i (x i) j = x j
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case h.refine'_3.h.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) i = x i
[PROOFSTEP]
exact Function.update_same _ _ _
[GOAL]
case h.refine'_3.h.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
j : ι
hij : i ≠ j
⊢ update f i (x i) j = x j
[PROOFSTEP]
simpa only [Function.update_noteq hij.symm, le_antisymm_iff] using h j (mem_univ j)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b = Ico (update f i a) (update f i b)
[PROOFSTEP]
rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton, image_update_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioc a b = Ioc (update f i a) (update f i b)
[PROOFSTEP]
rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton, image_update_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)
[PROOFSTEP]
rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton, image_update_Ico]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Icc a (f i) = Icc (update f i a) f
[PROOFSTEP]
simpa using image_update_Icc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ico a (f i) = Ico (update f i a) f
[PROOFSTEP]
simpa using image_update_Ico f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioc a (f i) = Ioc (update f i a) f
[PROOFSTEP]
simpa using image_update_Ioc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioo a (f i) = Ioo (update f i a) f
[PROOFSTEP]
simpa using image_update_Ioo f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Icc (f i) b = Icc f (update f i b)
[PROOFSTEP]
simpa using image_update_Icc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ico (f i) b = Ico f (update f i b)
[PROOFSTEP]
simpa using image_update_Ico f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioc (f i) b = Ioc f (update f i b)
[PROOFSTEP]
simpa using image_update_Ioc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioo (f i) b = Ioo f (update f i b)
[PROOFSTEP]
simpa using image_update_Ioo f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)
[PROOFSTEP]
simp_rw [uIcc, update_sup, update_inf]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' uIcc a (f i) = uIcc (update f i a) f
[PROOFSTEP]
simpa using image_update_uIcc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' uIcc (f i) b = uIcc f (update f i b)
[PROOFSTEP]
simpa using image_update_uIcc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
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)
[PROOFSTEP]
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]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' : (i : ι) → α i
⊢ (Icc x y \ pi univ fun i => Ioo (x' i) (y' i)) ⊆
    (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
rintro a ⟨⟨hxa, hay⟩, ha'⟩
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
ha' : ¬a ∈ pi univ fun i => Ioo (x' i) (y' i)
hxa : x ≤ a
hay : a ≤ y
⊢ a ∈ (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
simp at ha' 
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, x' x < a x → y' x ≤ a x
⊢ a ∈ (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
simp [le_update_iff, update_le_iff, hxa, hay, hxa _, hay _, ← exists_or]
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, x' x < a x → y' x ≤ a x
⊢ ∃ x, a x ≤ x' x ∨ y' x ≤ a x
[PROOFSTEP]
rcases ha' with ⟨w, hw⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
⊢ ∃ x, a x ≤ x' x ∨ y' x ≤ a x
[PROOFSTEP]
apply Exists.intro w
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
cases lt_or_le (x' w) (a w)
[GOAL]
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
h✝ : x' w < a w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
simp_all
[GOAL]
case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
h✝ : a w ≤ x' w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
simp_all
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ pi univ fun i => Ioc (y i) (z i)) ⊆ ⋃ (i : ι), Icc x (update z i (y i))
[PROOFSTEP]
rintro a ⟨⟨hax, haz⟩, hay⟩
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : ¬a ∈ pi univ fun i => Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ a ∈ ⋃ (i : ι), Icc x (update z i (y i))
[PROOFSTEP]
simpa [not_and_or, hax, le_update_iff, haz _] using hay
