Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_QuasiPeriodic_eq (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
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
⊢ f (x + d) = f (x + c)
Tactic:
have h3 (c) := (iff_right hf.toNontrivialGood (c := c)).mp
State after:
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
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
h3 : ∀ (c : R), QuasiPeriodic f c → ∀ (x : R), f (x + c) = f x * -f c
⊢ f (x + d) = f (x + c)

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
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
h3 : ∀ (c : R), QuasiPeriodic f c → ∀ (x : R), f (x + c) = f x * -f c
⊢ f (x + d) = f (x + c)
Tactic:
rw [h3 c h, h3 d h1, h2, reduced_map_eq_one hf h h0]
State after:
no goals