no goals
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
h : a < 0
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha✝ : a ≠ 0
b c : α
ha : 0 < a
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]