[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a) (Ici (a + d))
[PROOFSTEP]
refine' ⟨fun x h => add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).injOn _, fun _ h => _⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d x✝ : M
h : x✝ ∈ Ici (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h 
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a ≤ a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
exact ⟨a + c, h, by rw [add_right_comm]⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a ≤ a + c
⊢ (fun x => x + d) (a + c) = a + d + c
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a) (Ioi (a + d))
[PROOFSTEP]
refine' ⟨fun x h => add_lt_add_right (mem_Ioi.mp h) _, fun _ _ _ _ h => add_right_cancel h, fun _ h => _⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d x✝ : M
h : x✝ ∈ Ioi (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h 
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a < a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
exact ⟨a + c, h, by rw [add_right_comm]⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a < a + c
⊢ (fun x => x + d) (a + c) = a + d + c
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Icc a b) (Icc (a + d) (b + d))
[PROOFSTEP]
rw [← Ici_inter_Iic, ← Ici_inter_Iic]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
[PROOFSTEP]
exact (Ici_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx => le_of_add_le_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioo a b) (Ioo (a + d) (b + d))
[PROOFSTEP]
rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))
[PROOFSTEP]
exact (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx => lt_of_add_lt_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioc a b) (Ioc (a + d) (b + d))
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
[PROOFSTEP]
exact (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx => le_of_add_le_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ico a b) (Ico (a + d) (b + d))
[PROOFSTEP]
rw [← Ici_inter_Iio, ← Ici_inter_Iio]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
[PROOFSTEP]
exact (Ici_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx => lt_of_add_lt_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ici b = Ici (a + b)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ici]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioi b = Ioi (a + b)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioi]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Icc b c = Icc (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Icc]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ico b c = Ico (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ico]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioc]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioo]
