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)
ι : 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)
ext x
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)
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)
rw [← Set.pi_univ_Icc]
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)

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

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
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)
refine' ⟨_, fun h => ⟨x i, _, _⟩⟩
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)
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)
rintro ⟨c, hc, rfl⟩
no goals
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)
simpa [update_le_update_iff]
no goals
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
simpa only [Function.update_same] using h i (mem_univ i)
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
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
ext j
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

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
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
obtain rfl | hij := eq_or_ne i j
no goals
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
exact Function.update_same _ _ _
no goals
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
simpa only [Function.update_noteq hij.symm, le_antisymm_iff] using h j (mem_univ j)