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
ι : 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
rintro a ⟨⟨hxa, hay⟩, ha'⟩
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
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
simp at ha'
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
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
simp [le_update_iff, update_le_iff, hxa, hay, hxa _, hay _, ← exists_or]
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
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
rcases ha' with ⟨w, hw⟩
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
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
apply Exists.intro w
no goals
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
cases lt_or_le (x' w) (a w) <;> simp_all