Theorem: IMOSL.IMO2012A5.PeriodEquiv.equiv_zero_iff (IMOSLLean4/IMO2012/A5/A5General/A5Periodic.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
⊢ (PeriodEquiv f) c 0 ↔ QuasiPeriodic f c ∧ f c = -1
Tactic:
rw [zero_right, QuasiPeriodic.iff_right hf]
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
⊢ (∀ (x : R), f (x + c) = f x) ↔ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1

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
⊢ (∀ (x : R), f (x + c) = f x) ↔ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
refine ⟨λ h ↦ ?_, λ h x ↦ by rw [h.1, h.2, neg_neg, mul_one]⟩
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) = f x
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1

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) = f x
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
have h0 : f c = -1 := by rw [← zero_add c, h, hf.map_zero]
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) = f x
h0 : f c = -1
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1

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) = f x
h0 : f c = -1
⊢ (∀ (x : R), f (x + c) = f x * -f c) ∧ f c = -1
Tactic:
refine ⟨λ x ↦ ?_, h0⟩
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) = f x
h0 : f c = -1
x : R
⊢ f (x + c) = f x * -f c

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) = f x
h0 : f c = -1
x : R
⊢ f (x + c) = f x * -f c
Tactic:
rw [h0, neg_neg, mul_one, h]
State after:
no goals

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) = f x * -f c) ∧ f c = -1
x : R
⊢ f (x + c) = f x
Tactic:
rw [h.1, h.2, neg_neg, mul_one]
State after:
no goals

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) = f x
⊢ f c = -1
Tactic:
rw [← zero_add c, h, hf.map_zero]
State after:
no goals