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

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

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

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

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

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

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

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

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