Theorem: IMOSL.IMO2012A5.Case2.CommCase.two_periodic_of_map_two (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
x : R
⊢ f (x * 2 + 1) = f (x + 2) - f x
Tactic:
rw [hf.is_good, h0, mul_neg_one, neg_add_eq_sub]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
x : R
⊢ f (x * 2 + 1) = -f (x * 2 - 1)
Tactic:
rw [Eq2 hf, Eq3 hf h, h0, mul_neg_one, mul_neg_one, neg_add_rev, neg_neg]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
have h3 := Eq4_alt hf h x
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x * f (x * 2 + 1) = (f (x + 1) + 1) * f (x * 2 - 1)
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
rw [h2, mul_neg, neg_eq_iff_add_eq_zero, ← add_mul, mul_eq_zero, ← add_assoc] at h3
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x + f (x + 1) + 1 = 0 ∨ f (x * 2 - 1) = 0
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
x : R
h3 : f x + f (x + 1) + 1 = 0 ∨ f (x * 2 - 1) = 0
⊢ f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
Tactic:
exact h3.imp_left eq_neg_of_add_eq_zero_left
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f ((x + 1) * 2 - 1) = 0
⊢ f (x + 2) = f x
Tactic:
rwa [mul_two, add_sub_assoc, add_sub_cancel_right,
add_right_comm, ← mul_two, h1, sub_eq_zero] at h4
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f (x + 1) + f (x + 1 + 1) = -1
h5 : f (x * 2 - 1) = 0
⊢ f (x + 2) = f x
Tactic:
rwa [← neg_eq_zero, ← h2, h1, sub_eq_zero] at h5
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
h0 : f 2 = -1
h1 : ∀ (x : R), f (x * 2 + 1) = f (x + 2) - f x
h2 : ∀ (x : R), f (x * 2 + 1) = -f (x * 2 - 1)
h3 : ∀ (x : R), f x + f (x + 1) = -1 ∨ f (x * 2 - 1) = 0
x : R
h4 : f (x + 1) + f (x + 1 + 1) = -1
h5 : f x + f (x + 1) = -1
⊢ f (x + 2) = f x
Tactic:
rwa [← h5, add_comm, add_left_inj, add_assoc, one_add_one_eq_two] at h4
State after:
no goals