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
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))
refine'
  ⟨fun x h => add_lt_add_right (mem_Ioi.mp h) _, fun _ _ _ _ h => add_right_cancel h, fun _ h =>
    _⟩
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
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
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
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
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
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h
no goals
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
exact ⟨a + c, h, by rw [add_right_comm]⟩
no goals
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
rw [add_right_comm]