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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
ys : List β
h1 : v ∈ []
⊢ updateListITE f [] ys v = updateListITE g [] ys v
Tactic:
case nil =>
  contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys : List β
h1 : v ∈ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = updateListITE g (xs_hd :: xs_tl) ys v
Tactic:
case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp at h1
    simp only [Function.updateListITE]
    exact h2
  case cons ys_hd ys_tl =>
    simp at h1
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    split_ifs
    case pos =>
      rfl
    case neg c1 =>
      cases h1
      case inl c2 =>
        contradiction
      case inr c2 =>
        exact xs_ih ys_tl c2
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
ys : List β
h1 : v ∈ []
⊢ updateListITE f [] ys v = updateListITE g [] ys v
Tactic:
contradiction
State after:
no goals

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v ∈ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = updateListITE g (xs_hd :: xs_tl) (ys_hd :: ys_tl) v
Tactic:
case cons ys_hd ys_tl =>
  simp at h1
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  split_ifs
  case pos =>
    rfl
  case neg c1 =>
    cases h1
    case inl c2 =>
      contradiction
    case inr c2 =>
      exact xs_ih ys_tl c2
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v ∈ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) [] v = updateListITE g (xs_hd :: xs_tl) [] v
Tactic:
simp at h1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) [] v = updateListITE g (xs_hd :: xs_tl) [] v

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v ∈ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = updateListITE g (xs_hd :: xs_tl) (ys_hd :: ys_tl) v
Tactic:
simp at h1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v = xs_hd ∨ v ∈ xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = updateListITE g (xs_hd :: xs_tl) (ys_hd :: ys_tl) v

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

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

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

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

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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v = xs_hd ∨ v ∈ xs_tl
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
case neg c1 =>
  cases h1
  case inl c2 =>
    contradiction
  case inr c2 =>
    exact xs_ih ys_tl c2
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v = xs_hd ∨ v ∈ xs_tl
h✝ : v = xs_hd
⊢ ys_hd = ys_hd
Tactic:
rfl
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v = xs_hd ∨ v ∈ xs_tl
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
cases h1
State after:
case inl
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h✝ : v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v

case inr
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
h✝ : v ∈ xs_tl
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
c2 : v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
case inl c2 =>
  contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
c2 : v ∈ xs_tl
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
case inr c2 =>
  exact xs_ih ys_tl c2
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
c2 : v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
contradiction
State after:
no goals

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
c1 : ¬v = xs_hd
c2 : v ∈ xs_tl
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
exact xs_ih ys_tl c2
State after:
no goals