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

State before:
R : Type ?u.3631
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) = f c
⊢ f 0 = -(f c * f c)
Tactic:
cases h with
| Left h => specialize h (-c); rwa [add_neg_self, h0, neg_mul] at h
| Right h => specialize h (-c); rwa [neg_add_self, h0, mul_neg] at h
State after:
no goals

State before:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : ∀ (x : R), f (c + x) = -f c * f x
⊢ f 0 = -(f c * f c)
Tactic:
specialize h (-c)
State after:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (c + -c) = -f c * f (-c)
⊢ f 0 = -(f c * f c)

State before:
case Left
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (c + -c) = -f c * f (-c)
⊢ f 0 = -(f c * f c)
Tactic:
rwa [add_neg_self, h0, neg_mul] at h
State after:
no goals

State before:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : ∀ (x : R), f (x + c) = f x * -f c
⊢ f 0 = -(f c * f c)
Tactic:
specialize h (-c)
State after:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (-c + c) = f (-c) * -f c
⊢ f 0 = -(f c * f c)

State before:
case Right
R : Type ?u.3631
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h0 : f (-c) = f c
h : f (-c + c) = f (-c) * -f c
⊢ f 0 = -(f c * f c)
Tactic:
rwa [neg_add_self, h0, mul_neg] at h
State after:
no goals

State before:
R : Type ?u.3631
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) = f c
h1 : f 0 = -(f c * f c)
⊢ f c * f c = 1
Tactic:
rwa [hf.map_zero, neg_inj, eq_comm] at h1
State after:
no goals