Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_eq_zero_iff (IMOSLLean4/IMO2012/A5/A5General/A5QuasiPeriodic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0✝ : c ≠ 0
h0 : f c = -1
x : R
⊢ f (x + c) = f (x + 0)
Tactic:
rw [add_zero, (iff_right hf.toNontrivialGood).mp h, h0, neg_neg, mul_one]
State after:
no goals