-- Mathlib/Data/List/Nodup.lean
theorem Nodup.map_update [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) :
    l.map (Function.update f x y) =
      if x ∈ l then (l.map f).set (l.idxOf x) y else l.map f

Proof state:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
subst hd

Result:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : x ∉ tl ∧ tl.Nodup
⊢ (update f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
f : α → β
x : α
y : β
⊢ map (update f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l

Tactic:
induction' l with hd tl ihl

Result:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hl : [].Nodup
⊢ map (update f x y) [] = if x ∈ [] then (map f []).set (idxOf x []) y else map f []

case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Proof state:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
simp only [mem_cons, map, ihl hl.2]

Result:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Proof state:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
rw [nodup_cons] at hl

Result:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Proof state:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
by_cases H : hd = x

Result:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Proof state:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : hd ∉ tl ∧ tl.Nodup
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
simp [Ne.symm H, H, set, ← apply_ite (cons (f hd))]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hl : [].Nodup
⊢ map (update f x y) [] = if x ∈ [] then (map f []).set (idxOf x []) y else map f []

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : x ∉ tl ∧ tl.Nodup
⊢ (update f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl

Tactic:
simp [set, hl.1]

Result:
no goals