case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hl : Nodup []
⊢ map (update f x y) [] = if x ∈ [] then set (map f []) (indexOf x []) y else map f []

case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : Nodup (hd :: tl)
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl : Nodup l
f : α → β
x : α
y : β
⊢ map (update f x y) l = if x ∈ l then set (map f l) (indexOf x l) y else map f l
induction' l with hd tl ihl
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : Nodup (hd :: tl)
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
rw [nodup_cons] at hl
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then set (map f (hd :: tl)) (indexOf x (hd :: tl)) y else map f (hd :: tl)
simp only [mem_cons, map, ihl hl.2]
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl

case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
by_cases H : hd = x
no goals
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hl : Nodup []
⊢ map (update f x y) [] = if x ∈ [] then set (map f []) (indexOf x []) y else map f []
simp
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ Nodup tl
⊢ (update f x y x :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then set (f x :: map f tl) (indexOf x (x :: tl)) y else f x :: map f tl
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
subst hd
no goals
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ Nodup tl
⊢ (update f x y x :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then set (f x :: map f tl) (indexOf x (x :: tl)) y else f x :: map f tl
simp [set, hl.1]
no goals
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l : List α
hl✝ : Nodup l
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : Nodup tl → map (update f x y) tl = if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ Nodup tl
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then set (map f tl) (indexOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then set (f hd :: map f tl) (indexOf x (hd :: tl)) y else f hd :: map f tl
simp [Ne.symm H, H, set, ← apply_ite (cons (f hd))]