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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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]
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

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
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

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals