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

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : ∀ (d : R), d * c = 0 → QuasiPeriodic f d := fun d => reduced_mul_left_eq_zero_imp hf h h0
h2 : d * c = c
⊢ (d - 1) * c = 0
Tactic:
rwa [sub_one_mul, sub_eq_zero]
State after:
no goals