[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Icc a b = Icc (-b) (-a)
[PROOFSTEP]
simp [← Ici_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ico a b = Ioc (-b) (-a)
[PROOFSTEP]
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ioc a b = Ico (-b) (-a)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ -Ioo a b = Ioo (-b) (-a)
[PROOFSTEP]
simp [← Ioi_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ici b = Ici (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Iic b = Iic (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Iio b = Iio (b + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
simp [← Ici_inter_Iic, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
simp [← Ioi_inter_Iio, inter_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) '' Iic b = Iic (a + b)
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) '' Iio b = Iio (a + b)
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) '' Iic b = Iic (b + a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) '' Iio b = Iio (b + a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ici a = Iic (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Iic a = Ici (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioi a = Iio (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Iio a = Ioi (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Icc a b = Icc (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ico a b = Ioc (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioc a b = Ico (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ Neg.neg '' Ioo a b = Ioo (-b) (-a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ici b = Iic (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iic b = Ici (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ici b = Ici (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Iic b = Iic (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioi b = Ioi (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Iio b = Iio (b - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Icc b c = Icc (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ico b c = Ico (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)
[PROOFSTEP]
simp [sub_eq_neg_add]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simpa only [add_comm] using preimage_const_add_uIcc a b c
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ -[[a, b]] = [[-a, -b]]
[PROOFSTEP]
simp only [← Icc_min_max, preimage_neg_Icc, min_neg_neg, max_neg_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
simp_rw [← Icc_min_max, preimage_const_sub_Icc]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))
[PROOFSTEP]
simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a + x) '' [[b, c]] = [[a + b, a + c]]
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x + a) '' [[b, c]] = [[b + a, c + a]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
have := image_comp (fun x => a + x) fun x => -x
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
[PROOFSTEP]
simp [sub_eq_add_neg, this, add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ (fun x => x - a) '' [[b, c]] = [[b - a, c - a]]
[PROOFSTEP]
simp [sub_eq_add_neg, add_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ Neg.neg '' [[a, b]] = [[-a, -b]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ |d - c| ≤ |b - a|
[PROOFSTEP]
rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b
[PROOFSTEP]
rw [uIcc_subset_uIcc_iff_le] at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : min a b ≤ min c d ∧ max c d ≤ max a b
⊢ max c d - min c d ≤ max a b - min a b
[PROOFSTEP]
exact sub_le_sub h.2 h.1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h, inter_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioo a b = Ioo (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioc a b = Ioc (a / c) (b / c)
[PROOFSTEP]
simp [← Ioi_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ico a b = Ico (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iio, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ (fun x x_1 => x * x_1) c ⁻¹' Icc a b = Icc (a / c) (b / c)
[PROOFSTEP]
simp [← Ici_inter_Iic, h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Iio a = Ioi (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioi a = Iio (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Iic a = Ici (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ici a = Iic (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioo a b = Ioo (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ioc a b = Ico (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Ico a b = Ioc (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : c < 0
⊢ (fun x x_1 => x * x_1) c ⁻¹' Icc a b = Icc (b / c) (a / c)
[PROOFSTEP]
simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
h : a < 0
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha✝ : a ≠ 0
b c : α
ha : 0 < a
⊢ (fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp only [← preimage_mul_const_uIcc ha, mul_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
[PROOFSTEP]
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : a = 0
⊢ (fun x => x * a) '' [[b, c]] = [[b * a, c * a]]
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : ¬a = 0
⊢ (fun x => x * a⁻¹) ⁻¹' [[b, c]] = (fun x => x / a) ⁻¹' [[b, c]]
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
⊢ (fun x => a * x) '' [[b, c]] = [[a * b, a * c]]
[PROOFSTEP]
simpa only [mul_comm] using image_mul_const_uIcc a b c
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
⊢ (fun x => x / a) '' [[b, c]] = [[b / a, c / a]]
[PROOFSTEP]
simp only [div_eq_mul_inv, image_mul_const_uIcc]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ ↑(Units.mulRight (Units.mk0 c (_ : c ≠ 0))).symm ⁻¹' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
simp [h, division_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
cases eq_or_lt_of_le hc
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 = c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
subst c
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b : α
hab : a ≤ b
hc : 0 ≤ 0
⊢ (fun x => x * 0) '' Icc a b = Icc (a * 0) (b * 0)
[PROOFSTEP]
simp [(nonempty_Icc.2 hab).image_const]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
hab : a ≤ b
hc : 0 ≤ c
h✝ : 0 < c
⊢ (fun x => x * c) '' Icc a b = Icc (a * c) (b * c)
[PROOFSTEP]
exact image_mul_right_Icc' a b ‹0 < c›
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Icc b c = Icc (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Icc' b c h using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Icc b c = (fun x => x * a) '' Icc b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ Icc (a * b) (a * c) = Icc (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x x_1 => x * x_1) a '' Icc b c = Icc (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Icc hbc ha using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x x_1 => x * x_1) a '' Icc b c = (fun x => x * a) '' Icc b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
ha : 0 ≤ a
hbc : b ≤ c
⊢ Icc (a * b) (a * c) = Icc (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a b c : α
h : 0 < c
⊢ ↑(Units.mulRight (Units.mk0 c (_ : c ≠ 0))).symm ⁻¹' Ioo a b = Ioo (a * c) (b * c)
[PROOFSTEP]
simp [h, division_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Ioo b c = Ioo (a * b) (a * c)
[PROOFSTEP]
convert image_mul_right_Ioo b c h using 1
[GOAL]
case h.e'_2
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Ioo b c = (fun x => x * a) '' Ioo b c
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ Ioo (a * b) (a * c) = Ioo (b * a) (c * a)
[PROOFSTEP]
simp only [mul_comm _ a]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
x : α
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹
[PROOFSTEP]
exact
  ⟨fun h => inv_inv x ▸ (inv_lt_inv ha h.1).2 h.2, fun h =>
    ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_inv a ▸ (inv_lt_inv ((inv_pos.2 ha).trans h) (inv_pos.2 ha)).2 h⟩⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
ha : 0 < a
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
a : α
k : Type u_2
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0
[PROOFSTEP]
erw [(Units.mk0 x hx.ne').mulLeft.image_eq_preimage, preimage_const_mul_Ioi 0 (inv_pos.mpr hx), zero_div]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
⊢ (fun x => a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
suffices (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b) by
  rwa [Set.image_image] at this 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
rwa [Set.image_image] at this 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
[PROOFSTEP]
rw [image_mul_left_Icc' h, image_add_const_Icc]
