Theorem: Function.updateITE_not_mem_list (FOL/FunctionUpdateITE.lean)

State before:
α β : Type
inst✝ : DecidableEq α
xs : List α
f : α → β
a : α
b : β
h1 : a ∉ xs
⊢ List.map (updateITE f a b) xs = List.map f xs
Tactic:
induction xs
State after:
case nil
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []

case cons
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : a ∉ tail✝ → List.map (updateITE f a b) tail✝ = List.map f tail✝
h1 : a ∉ head✝ :: tail✝
⊢ List.map (updateITE f a b) (head✝ :: tail✝) = List.map f (head✝ :: tail✝)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []
Tactic:
case nil =>
  simp
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ∉ hd :: tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
case cons hd tl ih =>
  simp at h1
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    simp
    simp only [Function.updateITE]
    split_ifs <;> tauto
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
h1 : a ∉ []
⊢ List.map (updateITE f a b) [] = List.map f []
Tactic:
simp
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ∉ hd :: tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
simp at h1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : ¬a = hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : ¬a = hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
push_neg at h1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ≠ hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ≠ hd ∧ a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
cases h1
State after:
case intro
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
left✝ : a ≠ hd
right✝ : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
case intro h1_left h1_right =>
  simp
  simp only [Function.updateITE]
  split_ifs <;> tauto
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
Tactic:
simp
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ updateITE f a b hd = f hd ∧ List.map (updateITE f a b) tl = List.map f tl

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ updateITE f a b hd = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Tactic:
simp only [Function.updateITE]
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ (if hd = a then b else f hd) = f hd ∧ List.map (updateITE f a b) tl = List.map f tl

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1_left : a ≠ hd
h1_right : a ∉ tl
⊢ (if hd = a then b else f hd) = f hd ∧ List.map (updateITE f a b) tl = List.map f tl
Tactic:
split_ifs <;> tauto
State after:
no goals