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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
xs : List α
ys : List β
h1 : v ∉ xs
⊢ updateListITE f xs ys v = f v
Tactic:
induction xs generalizing ys
State after:
case nil
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
ys : List β
h1 : v ∉ []
⊢ updateListITE f [] ys v = f v

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
ys : List β
h1 : v ∉ []
⊢ updateListITE f [] ys v = f v
Tactic:
case nil =>
  simp only [Function.updateListITE]
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys : List β
h1 : v ∉ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = f v
Tactic:
case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [Function.updateListITE]
  case cons ys_hd ys_tl =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    split_ifs
    case pos c1 =>
      subst c1
      simp at h1
    case neg c1 =>
      simp at h1
      push_neg at h1
      cases h1
      case intro h1_left h1_right =>
        apply xs_ih ys_tl h1_right
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
ys : List β
h1 : v ∉ []
⊢ updateListITE f [] ys v = f v
Tactic:
simp only [Function.updateListITE]
State after:
no goals

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = f v
Tactic:
case cons ys_hd ys_tl =>
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  split_ifs
  case pos c1 =>
    subst c1
    simp at h1
  case neg c1 =>
    simp at h1
    push_neg at h1
    cases h1
    case intro h1_left h1_right =>
      apply xs_ih ys_tl h1_right
State after:
no goals

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

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
c1 : v = xs_hd
⊢ ys_hd = f v
Tactic:
case pos c1 =>
  subst c1
  simp at h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
case neg c1 =>
  simp at h1
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    apply xs_ih ys_tl h1_right
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
c1 : v = xs_hd
⊢ ys_hd = f v
Tactic:
subst c1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
h1 : v ∉ v :: xs_tl
⊢ ys_hd = f v

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
h1 : v ∉ v :: xs_tl
⊢ ys_hd = f v
Tactic:
simp at h1
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
simp at h1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1 : ¬v = xs_hd ∧ v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1 : ¬v = xs_hd ∧ v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
push_neg at h1
State after:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1 : v ≠ xs_hd ∧ v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1 : v ≠ xs_hd ∧ v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
cases h1
State after:
case intro
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
left✝ : v ≠ xs_hd
right✝ : v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1_left : v ≠ xs_hd
h1_right : v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
case intro h1_left h1_right =>
  apply xs_ih ys_tl h1_right
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h1_left : v ≠ xs_hd
h1_right : v ∉ xs_tl
⊢ updateListITE f xs_tl ys_tl v = f v
Tactic:
apply xs_ih ys_tl h1_right
State after:
no goals