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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs : List α
x : α
h1 : x ∈ xs
⊢ updateListITE f xs (List.map g xs) x = g x
Tactic:
induction xs
State after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
x head✝ : α
tail✝ : List α
tail_ih✝ : x ∈ tail✝ → updateListITE f tail✝ (List.map g tail✝) x = g x
h1 : x ∈ head✝ :: tail✝
⊢ updateListITE f (head✝ :: tail✝) (List.map g (head✝ :: tail✝)) x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x
Tactic:
case nil =>
  simp at h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x ∈ hd :: tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
case cons hd tl ih =>
  simp at h1
  simp
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    subst c1
    rfl
  case _ c1 =>
    tauto
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x
Tactic:
simp at h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x ∈ hd :: tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
simp at h1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
simp
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (g hd :: List.map g tl) x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (g hd :: List.map g tl) x = g x
Tactic:
simp only [Function.updateListITE]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateITE (updateListITE f tl (List.map g tl)) hd (g hd) x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateITE (updateListITE f tl (List.map g tl)) hd (g hd) x = g x
Tactic:
simp only [Function.updateITE]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ (if x = hd then g hd else updateListITE f tl (List.map g tl) x) = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ (if x = hd then g hd else updateListITE f tl (List.map g tl) x) = g x
Tactic:
split_ifs
State after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
h✝ : x = hd
⊢ g hd = g x

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
h✝ : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : x = hd
⊢ g hd = g x
Tactic:
case _ c1 =>
  subst c1
  rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x
Tactic:
case _ c1 =>
  tauto
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : x = hd
⊢ g hd = g x
Tactic:
subst c1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = x ∨ x ∈ tl
⊢ g x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = x ∨ x ∈ tl
⊢ g x = g x
Tactic:
rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x
Tactic:
tauto
State after:
no goals