Theorem: IMOSL.IMO2012A5.Case2.CommCase.Eq4 (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
x : R
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
have h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1 := by
  rw [mul_add_one (x - 1), add_assoc, sub_add_cancel, sub_one_mul,
    ← add_sub_right_comm, add_comm, add_sub_add_right_eq_sub]
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
x : R
h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)

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
x : R
h0 : x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
apply congrArg f at h0
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
x : R
h0 : f (x * (x + 1) - 1) = f ((x - 1) * (x + 1 + 1) + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)

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
x : R
h0 : f (x * (x + 1) - 1) = f ((x - 1) * (x + 1 + 1) + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
rw [Eq1 hf h, hf.is_good, sub_add_cancel_left, h, hf.map_one, sub_add_add_cancel,
  add_zero, add_assoc, one_add_one_eq_two, ← add_assoc, ← mul_two] at h0
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
x : R
h0 : f x * f (x + 1) = f (x - 1) * f (x + 2) + f (x * 2 + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)

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
x : R
h0 : f x * f (x + 1) = f (x - 1) * f (x + 2) + f (x * 2 + 1)
⊢ f x * f (x * 2 - 1) = (f (x - 1) + 1) * f (x * 2 + 1)
Tactic:
rw [Eq2 hf, mul_add, h0, ← add_assoc, add_one_mul (f _),
  add_left_inj, mul_left_comm, ← mul_add, ← hf.is_good]
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
x : R
⊢ x * (x + 1) - 1 = (x - 1) * (x + 1 + 1) + 1
Tactic:
rw [mul_add_one (x - 1), add_assoc, sub_add_cancel, sub_one_mul,
  ← add_sub_right_comm, add_comm, add_sub_add_right_eq_sub]
State after:
no goals