no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]