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

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
have s1 : List.map f ys = List.map g ys
State after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ List.map f ys = List.map g ys

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x

State before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ List.map f ys = List.map g ys

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
simp only [List.map_eq_map_iff]
State after:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ ∀ x ∈ ys, f x = g x

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x

State before:
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
⊢ ∀ x ∈ ys, f x = g x

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
exact h1
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map g ys) x
Tactic:
simp only [s1]
State after:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map g ys) x = updateListITE g xs (List.map g ys) x

State before:
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ updateListITE f xs (List.map g ys) x = updateListITE g xs (List.map g ys) x
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case h1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ x ∈ xs

case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = (List.map g ys).length

State before:
case h1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ x ∈ xs
Tactic:
exact h2
State after:
no goals

State before:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = (List.map g ys).length
Tactic:
simp
State after:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = ys.length

State before:
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = ys.length
Tactic:
exact h3
State after:
no goals