-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Icc (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' Icc a b = Icc (update f i a) (update f i b)

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x

Tactic:
ext j

Result:
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 ∈ univ.pi 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

Proof state:
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)

Tactic:
rw [← Set.pi_univ_Icc]

Result:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

Tactic:
simpa only [Function.update_self] using h i (mem_univ i)

Result:
no goals

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)

Tactic:
simpa [update_le_update_iff]

Result:
no goals

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)

Tactic:
refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩

Result:
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 ∈ univ.pi 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 ∈ univ.pi 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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) i = x i

Tactic:
exact Function.update_self ..

Result:
no goals

Proof state:
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 ∈ univ.pi 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

Tactic:
simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using h j (mem_univ j)

Result:
no goals

Proof state:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
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 ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)

Proof state:
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 ∈ univ.pi 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

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
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 ∈ univ.pi 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 ∈ univ.pi 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

Proof state:
ι : 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)

Tactic:
ext x

Result:
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)