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

State before:
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
x : R
⊢ Commute (-f c) (f x)
Tactic:
cases map_eq_one_or_neg_one hf h with
| inl h => rw [h]; exact Commute.neg_one_left (f x)
| inr h => rw [h, neg_neg]; exact Commute.one_left (f x)
State after:
no goals

State before:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-f c) (f x)
Tactic:
rw [h]
State after:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-1) (f x)

State before:
case inl
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = 1
⊢ Commute (-1) (f x)
Tactic:
exact Commute.neg_one_left (f x)
State after:
no goals

State before:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute (-f c) (f x)
Tactic:
rw [h, neg_neg]
State after:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute 1 (f x)

State before:
case inr
R : Type ?u.6428
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h✝ : QuasiPeriodic f c
x : R
h : f c = -1
⊢ Commute 1 (f x)
Tactic:
exact Commute.one_left (f x)
State after:
no goals