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

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

case cons
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List β), updateListITE (updateITE f y z) tail✝ ys x = updateListITE f tail✝ ys x
ys : List β
⊢ updateListITE (updateITE f y z) (head✝ :: tail✝) ys x = updateListITE f (head✝ :: tail✝) ys x

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys : List β
⊢ updateListITE (updateITE f y z) (xs_hd :: xs_tl) ys x = updateListITE f (xs_hd :: xs_tl) ys x
Tactic:
case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    simp only [if_neg h1]
  case cons ys_hd ys_tl =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    split_ifs
    case pos c1 =>
      rfl
    case neg c1 =>
      apply xs_ih
State after:
no goals

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ updateITE f y z x = f x
Tactic:
simp only [Function.updateITE]
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ (if x = y then z else f x) = f x

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ (if x = y then z else f x) = f x
Tactic:
simp only [if_neg h1]
State after:
no goals

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

case cons
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
head✝ : β
tail✝ : List β
⊢ updateListITE (updateITE f y z) (xs_hd :: xs_tl) (head✝ :: tail✝) x =
    updateListITE f (xs_hd :: xs_tl) (head✝ :: tail✝) x

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
⊢ updateListITE (updateITE f y z) (xs_hd :: xs_tl) (ys_hd :: ys_tl) x =
    updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) x
Tactic:
case cons ys_hd ys_tl =>
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  split_ifs
  case pos c1 =>
    rfl
  case neg c1 =>
    apply xs_ih
State after:
no goals

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
⊢ (if x = y then z else f x) = f x
Tactic:
simp only [if_neg h1]
State after:
no goals

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
c1 : x = xs_hd
⊢ ys_hd = ys_hd
Tactic:
case pos c1 =>
  rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
c1 : ¬x = xs_hd
⊢ updateListITE (updateITE f y z) xs_tl ys_tl x = updateListITE f xs_tl ys_tl x
Tactic:
case neg c1 =>
  apply xs_ih
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
c1 : x = xs_hd
⊢ ys_hd = ys_hd
Tactic:
rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
c1 : ¬x = xs_hd
⊢ updateListITE (updateITE f y z) xs_tl ys_tl x = updateListITE f xs_tl ys_tl x
Tactic:
apply xs_ih
State after:
no goals