internlm/Lean-Github huggingface dataset:
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:
simp only [Function.updateListITE]
Proof 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
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
⊢ 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
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
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
⊢ (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_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]
Proof 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
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 β
⊢ 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]
Proof 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
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 β
⊢ (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
Proof 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
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 β
c1 : x = xs_hd
⊢ ys_hd = ys_hd
Tactic:
case pos c1 =>
  rfl
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 β
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
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 β
c1 : x = xs_hd
⊢ ys_hd = ys_hd
Tactic:
rfl
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 β
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
Proof state after:
no goals
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
have s1 : List.map f ys = List.map g ys
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ List.map f ys = List.map g ys

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ List.map f ys = List.map g ys

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ ∀ x ∈ ys, f x = g x

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ ∀ x ∈ ys, f x = g x

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
exact h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
simp only [s1]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map g ys) x = updateListITE g xs (List.map g ys) x
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map g ys) x = updateListITE g xs (List.map g ys) x
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case h1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ x ∈ xs

case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = (List.map g ys).length
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
case h1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ x ∈ xs
Tactic:
exact h2
Proof state after:
no goals
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = (List.map g ys).length
Tactic:
simp
Proof state after:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = ys.length
Theorem: Function.updateListITE_fun_coincide_mem_eq_len
Proof state before:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = ys.length
Tactic:
exact h3
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Tactic:
have s1 : List.map h ys = List.map h' ys
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ List.map h ys = List.map h' ys

α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ List.map h ys = List.map h' ys

α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ ∀ x ∈ ys, h x = h' x

α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ ∀ x ∈ ys, h x = h' x

α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Tactic:
exact h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h ys) x = updateListITE g xs (List.map h' ys) x
Tactic:
simp only [s1]
Proof state after:
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h' ys) x = updateListITE g xs (List.map h' ys) x
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ updateListITE f xs (List.map h' ys) x = updateListITE g xs (List.map h' ys) x
Tactic:
apply Function.updateListITE_mem_eq_len
Proof state after:
case h1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ x ∈ xs

case h2
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ xs.length = (List.map h' ys).length
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
case h1
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ x ∈ xs
Tactic:
exact h3
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
case h2
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ xs.length = (List.map h' ys).length
Tactic:
simp
Proof state after:
case h2
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ xs.length = ys.length
Theorem: Function.updateListITE_map_mem_ext
Proof state before:
case h2
α β : Type
inst✝ : DecidableEq α
xs ys : List α
f g h h' : α → β
x : α
h1 : ∀ y ∈ ys, h y = h' y
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : List.map h ys = List.map h' ys
⊢ xs.length = ys.length
Tactic:
exact h2
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs : List α
x : α
h1 : x ∈ xs
⊢ updateListITE f xs (List.map g xs) x = g x
Tactic:
induction xs
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
x head✝ : α
tail✝ : List α
tail_ih✝ : x ∈ tail✝ → updateListITE f tail✝ (List.map g tail✝) x = g x
h1 : x ∈ head✝ :: tail✝
⊢ updateListITE f (head✝ :: tail✝) (List.map g (head✝ :: tail✝)) x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x
Tactic:
case nil =>
  simp at h1
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x ∈ hd :: tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
case cons hd tl ih =>
  simp at h1
  simp
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    subst c1
    rfl
  case _ c1 =>
    tauto
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : x ∈ []
⊢ updateListITE f [] (List.map g []) x = g x
Tactic:
simp at h1
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x ∈ hd :: tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
simp at h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (List.map g (hd :: tl)) x = g x
Tactic:
simp
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (g hd :: List.map g tl) x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (g hd :: List.map g tl) x = g x
Tactic:
simp only [Function.updateListITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateITE (updateListITE f tl (List.map g tl)) hd (g hd) x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateITE (updateListITE f tl (List.map g tl)) hd (g hd) x = g x
Tactic:
simp only [Function.updateITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ (if x = hd then g hd else updateListITE f tl (List.map g tl) x) = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ (if x = hd then g hd else updateListITE f tl (List.map g tl) x) = g x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
h✝ : x = hd
⊢ g hd = g x

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
h✝ : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : x = hd
⊢ g hd = g x
Tactic:
case _ c1 =>
  subst c1
  rfl
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x
Tactic:
case _ c1 =>
  tauto
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : x = hd
⊢ g hd = g x
Tactic:
subst c1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = x ∨ x ∈ tl
⊢ g x = g x
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = x ∨ x ∈ tl
⊢ g x = g x
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateListITE_map_mem
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
c1 : ¬x = hd
⊢ updateListITE f tl (List.map g tl) x = g x
Tactic:
tauto
Proof state after:
no goals
Theorem: Function.updateListITE_map_updateIte
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Tactic:
have s1 : ∀ (y : α), y ∈ ys → f y =Function.updateITE f v a y
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ ∀ y ∈ ys, f y = updateITE f v a y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Theorem: Function.updateListITE_map_updateIte
Proof state before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ ∀ y ∈ ys, f y = updateITE f v a y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
Tactic:
intro y a1
Proof state after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
⊢ f y = updateITE f v a y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x