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

State before:
R : Type u_2
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
⊢ f (-c) = f c
Tactic:
have h0 : f (c + 1) = 0 := by cases h with
| Left h => rw [h, hf.map_one, mul_zero]
| Right h => rw [add_comm, h, hf.map_one, zero_mul]
State after:
R : Type u_2
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
h0 : f (c + 1) = 0
⊢ f (-c) = f c

State before:
R : Type u_2
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
h0 : f (c + 1) = 0
⊢ f (-c) = f c
Tactic:
have h1 := hf.is_good (c + 1) (-1)
State after:
R : Type u_2
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
h0 : f (c + 1) = 0
h1 : f ((c + 1) * -1 + 1) = f (c + 1) * f (-1) + f (c + 1 + -1)
⊢ f (-c) = f c

State before:
R : Type u_2
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
h0 : f (c + 1) = 0
h1 : f ((c + 1) * -1 + 1) = f (c + 1) * f (-1) + f (c + 1 + -1)
⊢ f (-c) = f c
Tactic:
rwa [h0, zero_mul, zero_add, add_neg_cancel_right,
  mul_neg_one, neg_add_rev, neg_add_cancel_comm] at h1
State after:
no goals

State before:
R : Type u_2
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
⊢ f (c + 1) = 0
Tactic:
cases h with
| Left h => rw [h, hf.map_one, mul_zero]
| Right h => rw [add_comm, h, hf.map_one, zero_mul]
State after:
no goals

State before:
case Left
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
⊢ f (c + 1) = 0
Tactic:
rw [h, hf.map_one, mul_zero]
State after:
no goals

State before:
case Right
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (x + c) = f x * -f c
⊢ f (c + 1) = 0
Tactic:
rw [add_comm, h, hf.map_one, zero_mul]
State after:
no goals