Theorem: List.map_modifyLast (One.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
if heq: l = [] then
  simp only [heq, map, modifyLast_nil]
else
  rw [← List.dropLast_append_getLast heq, List.modifyLast_append_one, map_append, map_append,
    map_singleton, map_singleton,List.modifyLast_append_one, P.eq]
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
heq : l = []
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
simp only [heq, map, modifyLast_nil]
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
heq : ¬l = []
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
rw [← List.dropLast_append_getLast heq, List.modifyLast_append_one, map_append, map_append,
  map_singleton, map_singleton,List.modifyLast_append_one, P.eq]
State after:
no goals