internlm/Lean-Github huggingface dataset:
Theorem: Function.updateListITE_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_mem
Proof 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]
Proof 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
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_mem
Proof 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]
Proof 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
Theorem: Function.updateListITE_mem
Proof 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]
Proof 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
Theorem: Function.updateListITE_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
ys : List β
h1 : v ∉ []
⊢ updateListITE f [] ys v = f v
Tactic:
case nil =>
  simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
ys : List β
h1 : v ∉ []
⊢ updateListITE f [] ys v = f v
Tactic:
simp only [Function.updateListITE]
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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]
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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]
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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]
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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]
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_not_mem
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_updateIte
Proof 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
Proof 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
Theorem: Function.updateListITE_updateIte
Proof 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]
Proof state after:
no goals
Theorem: Function.updateListITE_updateIte
Proof 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
Proof state after:
no goals
Theorem: Function.updateListITE_updateIte
Proof 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]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ updateITE f y z x = f x
Theorem: Function.updateListITE_updateIte
Proof 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]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ (if x = y then z else f x) = f x
Theorem: Function.updateListITE_updateIte
Proof 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]
Proof state after:
no goals
Theorem: Function.updateListITE_updateIte
Proof 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
Proof 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
Theorem: Function.updateListITE_updateIte
Proof 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]
Proof state after:
no goals
Theorem: Function.updateListITE_updateIte
Proof 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
Proof state after:
no goals