Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase21.solution (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
⊢ f (x + 2) = -f x
Tactic:
have h0 := hf.toGoodCase2.Eq6 (x + 1)
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 2) = -f x

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 1 + 1) + f (x + 1 - 1) = (f (x + 1) + 1) * (f 2 - 1)
⊢ f (x + 2) = -f x
Tactic:
rw [h, sub_self, mul_zero, add_sub_cancel_right, add_assoc, one_add_one_eq_two] at h0
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 2) + f x = 0
⊢ f (x + 2) = -f x

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
x : R
h0 : f (x + 2) + f x = 0
⊢ f (x + 2) = -f x
Tactic:
exact eq_neg_iff_add_eq_zero.mpr h0
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
⊢ f (x + 4) = f x
Tactic:
have h1 : (2 : R) + 2 = 4 := by norm_num
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
h1 : 2 + 2 = 4
⊢ f (x + 4) = f x

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
h1 : 2 + 2 = 4
⊢ f (x + 4) = f x
Tactic:
rw [← h1, ← add_assoc, h0, h0, neg_neg]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
x : R
⊢ 2 + 2 = 4
Tactic:
norm_num
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
x : R
⊢ f (x + 2) = f x * -f 2
Tactic:
rw [h0, h, mul_neg_one]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
h2 : QuasiPeriodic f 2
⊢ 2 + 1 = -1
Tactic:
rwa [two_add_one_eq_three, eq_neg_iff_add_eq_zero, three_add_one_eq_four]
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : Function.Bijective ℤ₄.cast
⊢ f ℤ₄.ℤ₄0.cast = ↑(ℤ₄Map ℤ₄.ℤ₄0)
Tactic:
change f 0 = ((-1 : ℤ) : S)
State after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : Function.Bijective ℤ₄.cast
⊢ f 0 = ↑(-1)

State before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 1
h0 : ∀ (x : R), f (x + 2) = -f x
h1 : 4 = 0
hInj : Function.Injective ℤ₄.cast
hSurj : Function.Surjective ℤ₄.cast
h2 : Function.Bijective ℤ₄.cast
⊢ f 0 = ↑(-1)
Tactic:
rw [hf.map_zero, Int.cast_neg, Int.cast_one]
State after:
no goals