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

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

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

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 : α
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
Tactic:
simp only [Function.updateITE]
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 = if y = v then a else f 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

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 : α
a1 : y ∈ ys
⊢ f y = if y = v then a else f 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:
split_ifs
State after:
case pos
α β : 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
h✝ : y = v
⊢ f y = a

case neg
α β : 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
h✝ : ¬y = v
⊢ f y = f 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

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
y : α
a1 : y ∈ ys
c1 : y = v
⊢ f y = a
Tactic:
case _ c1 =>
  specialize h1 y a1
  contradiction
State after:
no goals

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
y : α
a1 : y ∈ ys
c2 : ¬y = v
⊢ f y = f y
Tactic:
case _ c2 =>
  rfl
State after:
no goals

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
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:
exact Function.updateListITE_map_mem_ext xs ys f g f (Function.updateITE f v a) x s1 h2 h3
State after:
no goals

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
y : α
a1 : y ∈ ys
c1 : y = v
⊢ f y = a
Tactic:
specialize h1 y a1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
h1 : ¬y = v
⊢ f y = a

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c1 : y = v
h1 : ¬y = v
⊢ f y = a
Tactic:
contradiction
State after:
no goals

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
y : α
a1 : y ∈ ys
c2 : ¬y = v
⊢ f y = f y
Tactic:
rfl
State after:
no goals