Theorem: IMOSL.IMO2012A5.Case1.GoodSubcase12.eq_zero_of_map_add_one (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
⊢ x = 0
Tactic:
have h0 (x) : f (-x) = f (x + 1) + f x := by
  rw [Eq1 hf.toNontrivialGood, hf.map_neg_one, mul_one]
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ x = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ x = 0
Tactic:
have h1 : f (-x) = f x := by rw [h0, h, zero_add]
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
⊢ x = 0

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
⊢ x = 0
Tactic:
refine hf.period_imp_zero λ y ↦ ?_
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
⊢ f (y + x) = f y

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
⊢ f (y + x) = f y
Tactic:
have h2 := Eq3 hf.toNontrivialGood x (y - 1)
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
h2 : f (-x) * f (-(y - 1)) + f (-(x + (y - 1))) = f x * f (y - 1) + f (x + (y - 1))
⊢ f (y + x) = f y

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
h1 : f (-x) = f x
y : R
h2 : f (-x) * f (-(y - 1)) + f (-(x + (y - 1))) = f x * f (y - 1) + f (x + (y - 1))
⊢ f (y + x) = f y
Tactic:
rwa [h1, Case1.Eq6 hf.toNontrivialGood (map_neg_one_ne_zero hf) h, neg_one_mul,
  neg_one_mul, h0, h0 (x + _), add_assoc, sub_add_cancel, ← add_assoc, add_left_inj,
  neg_add_rev, add_assoc, add_right_eq_self, neg_add_eq_zero, eq_comm, add_comm] at h2
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 : GoodSubcase12 f
x✝ : R
h : f (x✝ + 1) = 0
x : R
⊢ f (-x) = f (x + 1) + f x
Tactic:
rw [Eq1 hf.toNontrivialGood, hf.map_neg_one, mul_one]
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 : GoodSubcase12 f
x : R
h : f (x + 1) = 0
h0 : ∀ (x : R), f (-x) = f (x + 1) + f x
⊢ f (-x) = f x
Tactic:
rw [h0, h, zero_add]
State after:
no goals