Theorem: IMOSL.IMO2012A5.sub_one_solver (IMOSLLean4/IMO2012/A5/A5Answers/SubOneMap.lean)

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
suffices ∀ x y, f (x + y) = f x + f y + 1 by
  have h0 (x y) : f (x + y + 1) = f (x + 1) + f (y + 1) := by
    rw [h, h, h, this, add_assoc, add_add_add_comm]
  have h1 (x y) : f (x * y + 1) = f (x + 1) * f (y + 1) := by
    rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
      ← mul_add_one (f x), ← add_one_mul (f x)]
  exact ⟨⟨⟨⟨λ x ↦ f (x + 1), (h 1).trans <| by rw [hf.map_one, zero_add]⟩, h1⟩,
      ((h 0).trans hf.map_zero_add_one), h0⟩,
    λ x ↦ congrArg f (sub_add_cancel x 1).symm⟩
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h0 (x y) : f (x * y) + 1 = f x * f y + f (x + y) :=
  (h _).symm.trans (hf.is_good x y)
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h1 (x y) : f (x * y) = f x * f y + f (x + y) - 1 :=
  eq_sub_of_add_eq (h0 x y)
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h2 (x y) : f ((x + 1) * y) = f (x * y) + (f y + 1) := by
  rw [h1, h, add_right_comm, add_one_mul (f x), h, add_add_add_comm,
    ← h0, add_right_comm, add_sub_cancel_right]
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
intro x y
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x + y) = f x + f y + 1
Tactic:
have h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y)) := by
  rw [add_one_mul x, add_one_mul x, mul_add]
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
⊢ f (x + y) = f x + f y + 1

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
⊢ f (x + y) = f x + f y + 1
Tactic:
rwa [h2, h1, h2, mul_add, ← add_assoc, add_right_comm _ _ 1, h0, ← h,
  sub_eq_iff_eq_add, add_assoc, add_assoc, add_assoc, add_right_inj,
  ← add_left_inj 1, add_assoc, ← h, add_right_comm, ← mul_one_add (x + 1),
  h2, add_left_comm, mul_one_add x, add_assoc, add_right_inj, add_comm 1,
  h, mul_add_one (f x), h0, add_assoc, add_assoc (_ * _), add_right_inj,
  ← add_assoc, add_left_inj, ← add_assoc, eq_comm] at h3
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
have h0 (x y) : f (x + y + 1) = f (x + 1) + f (y + 1) := by
  rw [h, h, h, this, add_assoc, add_add_add_comm]
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
have h1 (x y) : f (x * y + 1) = f (x + 1) * f (y + 1) := by
  rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
    ← mul_add_one (f x), ← add_one_mul (f x)]
State after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
exact ⟨⟨⟨⟨λ x ↦ f (x + 1), (h 1).trans <| by rw [hf.map_one, zero_add]⟩, h1⟩,
    ((h 0).trans hf.map_zero_add_one), h0⟩,
  λ x ↦ congrArg f (sub_add_cancel x 1).symm⟩
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
x y : R
⊢ f (x + y + 1) = f (x + 1) + f (y + 1)
Tactic:
rw [h, h, h, this, add_assoc, add_add_add_comm]
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
x y : R
⊢ f (x * y + 1) = f (x + 1) * f (y + 1)
Tactic:
rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
  ← mul_add_one (f x), ← add_one_mul (f x)]
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ f 1 + 1 = 1
Tactic:
rw [hf.map_one, zero_add]
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
x y : R
⊢ f ((x + 1) * y) = f (x * y) + (f y + 1)
Tactic:
rw [h1, h, add_right_comm, add_one_mul (f x), h, add_add_add_comm,
  ← h0, add_right_comm, add_sub_cancel_right]
State after:
no goals

State before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
Tactic:
rw [add_one_mul x, add_one_mul x, mul_add]
State after:
no goals