Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_left (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 : NontrivialGood f
c : R
h : QuasiPeriodic f c
d : R
⊢ QuasiPeriodic f (d * c)
Tactic:
rw [iff_right2 hf] at h ⊢
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d : R
⊢ ∀ (x : R), f (x * (d * c) + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d : R
⊢ ∀ (x : R), f (x * (d * c) + 1) = 0
Tactic:
intro x
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d x : R
⊢ f (x * (d * c) + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d x : R
⊢ f (x * (d * c) + 1) = 0
Tactic:
rw [← mul_assoc]
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d x : R
⊢ f (x * d * c + 1) = 0

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x * c + 1) = 0
d x : R
⊢ f (x * d * c + 1) = 0
Tactic:
exact h (x * d)
State after:
no goals