no goals
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
    ((Finset.nodup _).map <| add_right_injective c).dedup]
no goals
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
((Finset.nodup _).map <| add_right_injective c).dedup]