no goals
α : Type u_1
β : Type u_2
γ : Type ?u.128430
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc : c ≠ 0
a : α
⊢ f '' uIcc a (a + c) = range f
cases hc.lt_or_lt with
| inl hc =>
  rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
    add_neg_cancel_right]
| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.128430
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' uIcc a (a + c) = range f
rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
  add_neg_cancel_right]
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.128430
f g : α → β
c c₁ c₂ x : α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f
rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]