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))
ι : 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))
rintro a ⟨⟨hax, haz⟩, hay⟩
no goals
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))
simpa [not_and_or, hax, le_update_iff, haz _] using hay