Theorem: IMOSL.IMO2015A2.final_solution (IMOSLLean4/IMO2015/A2/A2.lean)

State before:
f : ℤ → ℤ
⊢ (∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1) ↔ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
refine Iff.symm ⟨λ h x y ↦ ?_, λ h ↦ ?_⟩
State after:
case refine_1
f : ℤ → ℤ
h : (f = fun x => -1) ∨ f = fun x => x + 1
x y : ℤ
⊢ f (x - f y) = f (f x) - f y - 1

case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1

State before:
case refine_1
f : ℤ → ℤ
h : (f = fun x => -1) ∨ f = fun x => x + 1
x y : ℤ
⊢ f (x - f y) = f (f x) - f y - 1
Tactic:
rcases h with rfl | rfl
State after:
case refine_1.inl
x y : ℤ
⊢ (fun x => -1) (x - (fun x => -1) y) = (fun x => -1) ((fun x => -1) x) - (fun x => -1) y - 1

case refine_1.inr
x y : ℤ
⊢ (fun x => x + 1) (x - (fun x => x + 1) y) = (fun x => x + 1) ((fun x => x + 1) x) - (fun x => x + 1) y - 1

State before:
case refine_1.inl
x y : ℤ
⊢ (fun x => -1) (x - (fun x => -1) y) = (fun x => -1) ((fun x => -1) x) - (fun x => -1) y - 1
Tactic:
rw [sub_sub, neg_add_self, sub_zero]
State after:
no goals

State before:
case refine_1.inr
x y : ℤ
⊢ (fun x => x + 1) (x - (fun x => x + 1) y) = (fun x => x + 1) ((fun x => x + 1) x) - (fun x => x + 1) y - 1
Tactic:
rw [sub_sub, add_sub_add_right_eq_sub, add_sub_right_comm]
State after:
no goals

State before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
have h0 := h 0 (f 0)
State after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = f (f 0) - f (f 0) - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1

State before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = f (f 0) - f (f 0) - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
rw [sub_self, zero_sub 1] at h0
State after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1

State before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
replace h0 x : f (x + 1) = f (f x) := by
  have h1 := h x (0 - f (f 0))
  rwa [h0, sub_neg_eq_add (f (f x)), add_sub_cancel_right] at h1
State after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ (f = fun x => -1) ∨ f = fun x => x + 1

State before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
have h1 : ∀ n, f n = (f (-1) + 1) * n + f 0 := by
  refine Extra.IntIntLinearSolverAlt λ n ↦ ?_
  have h1 := h0 (n - f n - 1)
  rw [sub_add_cancel, sub_right_comm, h, ← h0, h (n - 1), ← h0,
    sub_add_cancel, sub_self, zero_sub, sub_eq_iff_eq_add] at h1
  exact eq_add_of_sub_eq h1
State after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
⊢ (f = fun x => -1) ∨ f = fun x => x + 1

State before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
refine (eq_or_ne (f (-1) + 1) 0).imp
  (λ h2 ↦ funext λ x ↦ ?_) (λ h2 ↦ funext λ x ↦ ?_)
State after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f x = -1

case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
⊢ f x = x + 1

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
⊢ f (x + 1) = f (f x)
Tactic:
have h1 := h x (0 - f (f 0))
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
h1 : f (x - f (0 - f (f 0))) = f (f x) - f (0 - f (f 0)) - 1
⊢ f (x + 1) = f (f x)

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
h1 : f (x - f (0 - f (f 0))) = f (f x) - f (0 - f (f 0)) - 1
⊢ f (x + 1) = f (f x)
Tactic:
rwa [h0, sub_neg_eq_add (f (f x)), add_sub_cancel_right] at h1
State after:
no goals

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
Tactic:
refine Extra.IntIntLinearSolverAlt λ n ↦ ?_
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
⊢ f (n + 1) = f (-1) + 1 + f n

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
have h1 := h0 (n - f n - 1)
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n - f n - 1 + 1) = f (f (n - f n - 1))
⊢ f (n + 1) = f (-1) + 1 + f n

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n - f n - 1 + 1) = f (f (n - f n - 1))
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
rw [sub_add_cancel, sub_right_comm, h, ← h0, h (n - 1), ← h0,
  sub_add_cancel, sub_self, zero_sub, sub_eq_iff_eq_add] at h1
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n + 1) - f n = f (-1) + 1
⊢ f (n + 1) = f (-1) + 1 + f n

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n + 1) - f n = f (-1) + 1
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
exact eq_add_of_sub_eq h1
State after:
no goals

State before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f x = -1
Tactic:
rw [h1, h2, Int.zero_mul, zero_add, ← eq_neg_of_add_eq_zero_left h2]
State after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f 0 = f (-1)

State before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f 0 = f (-1)
Tactic:
specialize h1 (-1)
State after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = (f (-1) + 1) * -1 + f 0
⊢ f 0 = f (-1)

State before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = (f (-1) + 1) * -1 + f 0
⊢ f 0 = f (-1)
Tactic:
rw [h2, Int.zero_mul, zero_add] at h1
State after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = f 0
⊢ f 0 = f (-1)

State before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = f 0
⊢ f 0 = f (-1)
Tactic:
exact h1.symm
State after:
no goals

State before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
⊢ f x = x + 1
Tactic:
specialize h0 x
State after:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : f (x + 1) = f (f x)
⊢ f x = x + 1

State before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : f (x + 1) = f (f x)
⊢ f x = x + 1
Tactic:
rw [h1, h1 (f x), add_left_inj, Int.mul_eq_mul_left_iff h2] at h0
State after:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : x + 1 = f x
⊢ f x = x + 1

State before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : x + 1 = f x
⊢ f x = x + 1
Tactic:
exact h0.symm
State after:
no goals