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
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))
refine'
  ⟨fun x h => add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).injOn _, fun _ h => _⟩
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
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
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
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
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
rw [mem_Ici, add_right_comm, add_le_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) '' Ici 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]