Theorem: Function.updateListITE_mem' (FOL/FunctionUpdateITE.lean)

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ f x = g x
Tactic:
exact h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f ys) x = updateListITE g (xs_hd :: xs_tl) (List.map f ys) x
Tactic:
cases ys
State after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
head✝ : α
tail✝ : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f (head✝ :: tail✝)) x =
    updateListITE g (xs_hd :: xs_tl) (List.map f (head✝ :: tail✝)) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x
Tactic:
case nil =>
  simp
  simp only [Function.updateListITE]
  exact h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f []) x = updateListITE g (xs_hd :: xs_tl) (List.map f []) x
Tactic:
simp
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) [] x = updateListITE g (xs_hd :: xs_tl) [] x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) [] x = updateListITE g (xs_hd :: xs_tl) [] x
Tactic:
simp only [Function.updateListITE]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ f x = g x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ f x = g x
Tactic:
exact h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f (ys_hd :: ys_tl)) x =
    updateListITE g (xs_hd :: xs_tl) (List.map f (ys_hd :: ys_tl)) x
Tactic:
simp
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x =
    updateListITE g (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x =
    updateListITE g (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x
Tactic:
simp only [Function.updateListITE]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateITE (updateListITE f xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x =
    updateITE (updateListITE g xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateITE (updateListITE f xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x =
    updateITE (updateListITE g xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x
Tactic:
simp only [Function.updateITE]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ (if x = xs_hd then f ys_hd else updateListITE f xs_tl (List.map f ys_tl) x) =
    if x = xs_hd then f ys_hd else updateListITE g xs_tl (List.map f ys_tl) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ (if x = xs_hd then f ys_hd else updateListITE f xs_tl (List.map f ys_tl) x) =
    if x = xs_hd then f ys_hd else updateListITE g xs_tl (List.map f ys_tl) x
Tactic:
split_ifs
State after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : x = xs_hd
⊢ f ys_hd = f ys_hd

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : ¬x = xs_hd
⊢ updateListITE f xs_tl (List.map f ys_tl) x = updateListITE g xs_tl (List.map f ys_tl) x

State before:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : x = xs_hd
⊢ f ys_hd = f ys_hd
Tactic:
rfl
State after:
no goals

State before:
case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : ¬x = xs_hd
⊢ updateListITE f xs_tl (List.map f ys_tl) x = updateListITE g xs_tl (List.map f ys_tl) x
Tactic:
exact xs_ih ys_tl
State after:
no goals