no goals
R : Type u_2
S : Type u_1
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
h : IsLeftRegular (↑abv 1)
⊢ (fun x => ↑abv 1 * x) (↑abv 1) = (fun x => ↑abv 1 * x) 1
simp [← map_mul]