Theorem: IMOSL.IMO2013N1.final_solution (IMOSLLean4/IMO2013/N1/N1.lean)

State before:
f : ℕ+ → ℕ+
⊢ (∀ (m n : ℕ+), m * m + f n ∣ m * f m + n) ↔ f = id
Tactic:
refine ⟨λ h ↦ funext λ n ↦ le_antisymm ?_ ?_,
  λ h m n ↦ h.symm ▸ dvd_refl (m * m + n)⟩
State after:
case refine_1
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ f n ≤ id n

case refine_2
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ id n ≤ f n

State before:
case refine_1
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ f n ≤ id n
Tactic:
specialize h (f n) n
State after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * f n + f n ∣ f n * f (f n) + n
⊢ f n ≤ id n

State before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * f n + f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
rw [← mul_add_one (α := ℕ+)] at h
State after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * (f n + 1) ∣ f n * f (f n) + n
⊢ f n ≤ id n

State before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n * (f n + 1) ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
replace h := (dvd_mul_right _ _).trans h
State after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ f n * f (f n) + n
⊢ f n ≤ id n

State before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ f n * f (f n) + n
⊢ f n ≤ id n
Tactic:
rw [PNat.dvd_iff, PNat.add_coe, PNat.mul_coe,
  Nat.dvd_add_right ⟨_, rfl⟩, ← PNat.dvd_iff] at h
State after:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ n
⊢ f n ≤ id n

State before:
case refine_1
f : ℕ+ → ℕ+
n : ℕ+
h : f n ∣ n
⊢ f n ≤ id n
Tactic:
exact PNat.le_of_dvd h
State after:
no goals

State before:
case refine_2
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
⊢ id n ≤ f n
Tactic:
rcases eq_or_ne n 1 with rfl | h0
State after:
case refine_2.inl
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
⊢ id 1 ≤ f 1

case refine_2.inr
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
h0 : n ≠ 1
⊢ id n ≤ f n

State before:
case refine_2.inl
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
⊢ id 1 ≤ f 1
Tactic:
exact (f 1).one_le
State after:
no goals

State before:
case refine_2.inr
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
n : ℕ+
h0 : n ≠ 1
⊢ id n ≤ f n
Tactic:
rcases PNat.exists_eq_succ_of_ne_one h0 with ⟨k, rfl⟩
State after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
k : ℕ+
h0 : k + 1 ≠ 1
⊢ id (k + 1) ≤ f (k + 1)

State before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
h : ∀ (m n : ℕ+), m * m + f n ∣ m * f m + n
k : ℕ+
h0 : k + 1 ≠ 1
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
replace h := PNat.le_of_dvd (h (k + 1) (k + 1))
State after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : (k + 1) * (k + 1) + f (k + 1) ≤ (k + 1) * f (k + 1) + (k + 1)
⊢ id (k + 1) ≤ f (k + 1)

State before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : (k + 1) * (k + 1) + f (k + 1) ≤ (k + 1) * f (k + 1) + (k + 1)
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
rw [add_one_mul (α := ℕ+), add_right_comm,
  add_assoc, add_one_mul (α := ℕ+), add_assoc] at h
State after:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : k * (k + 1) + (f (k + 1) + (k + 1)) ≤ k * f (k + 1) + (f (k + 1) + (k + 1))
⊢ id (k + 1) ≤ f (k + 1)

State before:
case refine_2.inr.intro
f : ℕ+ → ℕ+
k : ℕ+
h0 : k + 1 ≠ 1
h : k * (k + 1) + (f (k + 1) + (k + 1)) ≤ k * f (k + 1) + (f (k + 1) + (k + 1))
⊢ id (k + 1) ≤ f (k + 1)
Tactic:
exact le_of_mul_le_mul_left' <| le_of_add_le_add_right (α := ℕ+) h
State after:
no goals