Theorem: IMOSL.IMO2012A5.ReducedGood.period_imp_zero (IMOSLLean4/IMO2012/A5/A5Defs.lean)

State before:
R : Type u_1
S : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : Add S
inst✝² : Mul S
inst✝¹ : One S
inst✝ : Zero S
c : R
f : R → S
hf : ReducedGood f
h : ∀ (x : R), f (x + c) = f x
x : R
⊢ f (x + c) = f (x + 0)
Tactic:
rw [h, add_zero]
State after:
no goals