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

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs : List α
ys : List β
⊢ g ∘ updateListITE f xs ys = updateListITE (g ∘ f) xs (List.map g ys)
Tactic:
induction xs generalizing ys
State after:
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)

case cons
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List β), g ∘ updateListITE f tail✝ ys = updateListITE (g ∘ f) tail✝ (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (head✝ :: tail✝) ys = updateListITE (g ∘ f) (head✝ :: tail✝) (List.map g ys)

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)
Tactic:
case nil =>
  simp only [Function.updateListITE]
State after:
no goals

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) ys = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g ys)
Tactic:
case cons _ xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp
    simp only [Function.updateListITE]
  case cons ys_hd ys_tl =>
    simp
    simp only [Function.updateListITE]
    simp only [← xs_ih]
    apply Function.updateITE_comp_left
State after:
no goals

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)
Tactic:
simp only [Function.updateListITE]
State after:
no goals

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) ys = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g ys)
Tactic:
cases ys
State after:
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])

case cons
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
head✝ : β
tail✝ : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (head✝ :: tail✝) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (head✝ :: tail✝))

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

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (ys_hd :: ys_tl))
Tactic:
case cons ys_hd ys_tl =>
  simp
  simp only [Function.updateListITE]
  simp only [← xs_ih]
  apply Function.updateITE_comp_left
State after:
no goals

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])
Tactic:
simp
State after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) []

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) []
Tactic:
simp only [Function.updateListITE]
State after:
no goals

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (ys_hd :: ys_tl))
Tactic:
simp
State after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (g ys_hd :: List.map g ys_tl)

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

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd =
    updateITE (updateListITE (g ∘ f) xs_tl (List.map g ys_tl)) xs_hd (g ys_hd)
Tactic:
simp only [← xs_ih]
State after:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd = updateITE (g ∘ updateListITE f xs_tl ys_tl) xs_hd (g ys_hd)

State before:
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd = updateITE (g ∘ updateListITE f xs_tl ys_tl) xs_hd (g ys_hd)
Tactic:
apply Function.updateITE_comp_left
State after:
no goals