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

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
have h := eq_zero_or_map_neg_add_self hf
State after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
⊢ x = 0 ∨ x = 1 ∨ x = -1

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
⊢ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
refine (h x).imp_right λ h0 ↦ (h (x - 1)).imp eq_of_sub_eq_zero
  λ h1 ↦ eq_neg_of_add_eq_zero_left <| (h (x + 1)).resolve_right λ h2 ↦ ?_
State after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
⊢ False

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
⊢ False
Tactic:
replace h (x) : f x + f (x + 1) + f (x - 1) = 0 := by
  have h3 : (2 : R) = -1 := by
    rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
  rw [sub_eq_add_neg, ← h3, triple_sum_eq_zero hf]
State after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : ∀ (x : R), f x + f (x + 1) + f (x - 1) = 0
⊢ False

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : f x + f (x + 1) + f (x - 1) + (f (-x) + f (-x + 1) + f (-x - 1)) = 0 + 0
⊢ False
Tactic:
rw [add_zero, ← neg_add', add_right_comm (f _), add_add_add_comm,
  add_add_add_comm (f _), h0, h2, neg_add_eq_sub, ← neg_sub x, h1,
  one_add_one_eq_two, two_add_one_eq_three] at h
State after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : 3 = 0
⊢ False

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x : R
h0 : f x + f (-x) = 1
h1 : f (x - 1) + f (-(x - 1)) = 1
h2 : f (x + 1) + f (-(x + 1)) = 1
h : 3 = 0
⊢ False
Tactic:
exact hf.Schar h
State after:
no goals

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
⊢ f x + f (x + 1) + f (x - 1) = 0
Tactic:
have h3 : (2 : R) = -1 := by
  rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
State after:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
h3 : 2 = -1
⊢ f x + f (x + 1) + f (x - 1) = 0

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
h3 : 2 = -1
⊢ f x + f (x + 1) + f (x - 1) = 0
Tactic:
rw [sub_eq_add_neg, ← h3, triple_sum_eq_zero hf]
State after:
no goals

State before:
R : Type u_1
S : Type ?u.34262
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodSubcase12 f
x✝ : R
h : ∀ (x : R), x = 0 ∨ f x + f (-x) = 1
h0 : f x✝ + f (-x✝) = 1
h1 : f (x✝ - 1) + f (-(x✝ - 1)) = 1
h2 : f (x✝ + 1) + f (-(x✝ + 1)) = 1
x : R
⊢ 2 = -1
Tactic:
rw [eq_neg_iff_add_eq_zero, two_add_one_eq_three, Rchar hf]
State after:
no goals