no goals
α : Type u_1
β : Type u_3
γ : Type u_2
f g✝ : α → β
c c₁ c₂ x✝ : α
inst✝¹ : Add α
inst✝ : Add γ
h : Periodic f c
g : AddHom γ α
g_inv : α → γ
hg : RightInverse g_inv ↑g
x : γ
⊢ (f ∘ ↑g) (x + g_inv c) = (f ∘ ↑g) x
simp only [hg c, h (g x), map_add, comp_apply]