internlm/Lean-Github huggingface dataset:
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ updateListITE f (xs_hd :: xs_tl) [] x = updateListITE g (xs_hd :: xs_tl) [] x
Tactic:
simp only [Function.updateListITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ f x = g x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
⊢ f x = g x
Tactic:
exact h1
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (List.map f (ys_hd :: ys_tl)) x =
    updateListITE g (xs_hd :: xs_tl) (List.map f (ys_hd :: ys_tl)) x
Tactic:
simp
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x =
    updateListITE g (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateListITE f (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x =
    updateListITE g (xs_hd :: xs_tl) (f ys_hd :: List.map f ys_tl) x
Tactic:
simp only [Function.updateListITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateITE (updateListITE f xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x =
    updateITE (updateListITE g xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ updateITE (updateListITE f xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x =
    updateITE (updateListITE g xs_tl (List.map f ys_tl)) xs_hd (f ys_hd) x
Tactic:
simp only [Function.updateITE]
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ (if x = xs_hd then f ys_hd else updateListITE f xs_tl (List.map f ys_tl) x) =
    if x = xs_hd then f ys_hd else updateListITE g xs_tl (List.map f ys_tl) x
Theorem: Function.updateListITE_mem'
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ (if x = xs_hd then f ys_hd else updateListITE f xs_tl (List.map f ys_tl) x) =
    if x = xs_hd then f ys_hd else updateListITE g xs_tl (List.map f ys_tl) x
Tactic:
split_ifs
Proof state after:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : x = xs_hd
⊢ f ys_hd = f ys_hd

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : ¬x = xs_hd
⊢ updateListITE f xs_tl (List.map f ys_tl) x = updateListITE g xs_tl (List.map f ys_tl) x
Theorem: Function.updateListITE_mem'
Proof state before:
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : x = xs_hd
⊢ f ys_hd = f ys_hd
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateListITE_mem'
Proof state before:
case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : ¬x = xs_hd
⊢ updateListITE f xs_tl (List.map f ys_tl) x = updateListITE g xs_tl (List.map f ys_tl) x
Tactic:
exact xs_ih ys_tl
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
xs : List α
ys : List β
h1 : v ∈ xs
h2 : xs.length = ys.length
⊢ updateListITE f xs ys v = updateListITE g xs ys v
Tactic:
induction xs generalizing ys
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
ys : List β
h1 : v ∈ []
h2 : [].length = ys.length
⊢ updateListITE f [] ys v = updateListITE g [] ys v

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
v head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ys : List β), v ∈ tail✝ → tail✝.length = ys.length → updateListITE f tail✝ ys v = updateListITE g tail✝ ys v
ys : List β
h1 : v ∈ head✝ :: tail✝
h2 : (head✝ :: tail✝).length = ys.length
⊢ updateListITE f (head✝ :: tail✝) ys v = updateListITE g (head✝ :: tail✝) ys v
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
ys : List β
h1 : v ∈ []
h2 : [].length = ys.length
⊢ updateListITE f [] ys v = updateListITE g [] ys v
Tactic:
case nil =>
  contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys : List β
h1 : v ∈ xs_hd :: xs_tl
h2 : (xs_hd :: xs_tl).length = ys.length
⊢ 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 =>
  simp at h1
  cases ys
  case nil =>
    contradiction
  case cons ys_hd ys_tl =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    cases h1
    case inl h1 =>
      simp only [if_pos h1]
    case inr h1 =>
      split_ifs
      case pos =>
        rfl
      case neg c1 =>
        simp at h2
        exact xs_ih ys_tl h1 h2
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
ys : List β
h1 : v ∈ []
h2 : [].length = ys.length
⊢ updateListITE f [] ys v = updateListITE g [] ys v
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys : List β
h1 : v ∈ xs_hd :: xs_tl
h2 : (xs_hd :: xs_tl).length = ys.length
⊢ updateListITE f (xs_hd :: xs_tl) ys v = updateListITE g (xs_hd :: xs_tl) ys v
Tactic:
simp at h1
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys : List β
h2 : (xs_hd :: xs_tl).length = ys.length
h1 : v = xs_hd ∨ v ∈ xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = updateListITE g (xs_hd :: xs_tl) ys v
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys : List β
h2 : (xs_hd :: xs_tl).length = ys.length
h1 : v = xs_hd ∨ v ∈ xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = updateListITE g (xs_hd :: xs_tl) ys v
Tactic:
cases ys
Proof state after:
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
h2 : (xs_hd :: xs_tl).length = [].length
⊢ updateListITE f (xs_hd :: xs_tl) [] v = updateListITE g (xs_hd :: xs_tl) [] v

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
head✝ : β
tail✝ : List β
h2 : (xs_hd :: xs_tl).length = (head✝ :: tail✝).length
⊢ updateListITE f (xs_hd :: xs_tl) (head✝ :: tail✝) v = updateListITE g (xs_hd :: xs_tl) (head✝ :: tail✝) v
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
h2 : (xs_hd :: xs_tl).length = [].length
⊢ updateListITE f (xs_hd :: xs_tl) [] v = updateListITE g (xs_hd :: xs_tl) [] v
Tactic:
case nil =>
  contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ 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 only [Function.updateListITE]
  simp only [Function.updateITE]
  cases h1
  case inl h1 =>
    simp only [if_pos h1]
  case inr h1 =>
    split_ifs
    case pos =>
      rfl
    case neg c1 =>
      simp at h2
      exact xs_ih ys_tl h1 h2
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
h2 : (xs_hd :: xs_tl).length = [].length
⊢ updateListITE f (xs_hd :: xs_tl) [] v = updateListITE g (xs_hd :: xs_tl) [] v
Tactic:
contradiction
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ 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 xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ 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_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ 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 xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ (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_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v = xs_hd ∨ v ∈ xs_tl
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
⊢ (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:
cases h1
Proof state after:
case inl
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h✝ : v = xs_hd
⊢ (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

case inr
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h✝ : 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_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v = xs_hd
⊢ (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:
case inl h1 =>
  simp only [if_pos h1]
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : 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:
case inr h1 =>
  split_ifs
  case pos =>
    rfl
  case neg c1 =>
    simp at h2
    exact xs_ih ys_tl h1 h2
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v = xs_hd
⊢ (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:
simp only [if_pos h1]
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : 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 xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v ∈ xs_tl
h✝ : v = xs_hd
⊢ ys_hd = ys_hd

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : 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_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v ∈ xs_tl
h✝ : v = xs_hd
⊢ ys_hd = ys_hd
Tactic:
case pos =>
  rfl
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : 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 =>
  simp at h2
  exact xs_ih ys_tl h1 h2
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v ∈ xs_tl
h✝ : v = xs_hd
⊢ ys_hd = ys_hd
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v ∈ xs_tl
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
simp at h2
Proof state after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v ∈ xs_tl
c1 : ¬v = xs_hd
h2 : xs_tl.length = ys_tl.length
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Theorem: Function.updateListITE_mem_eq_len
Proof state before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v ∈ xs_tl
c1 : ¬v = xs_hd
h2 : xs_tl.length = ys_tl.length
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
Tactic:
exact xs_ih ys_tl h1 h2
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
Proof 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
Theorem: Function.updateListITE_mem
Proof 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
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 : 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
Proof state after:
no goals
Theorem: Function.updateListITE_mem
Proof 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
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 : 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
Proof 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
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:
case nil =>
  simp at h1
  simp only [Function.updateListITE]
  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:
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
Proof state after:
no goals