English
If n > 0, there exist a,b > 0 with (b+1)^2 (a+1) = n and Squarefree (a+1).
Русский
Если n > 0, существует пара a,b > 0 такая, что (b+1)^2 (a+1) = n и Squarefree(a+1).
LaTeX
$$$\\exists a,b \\,(a>0) \\land (b>0) \\land ((b+1)^2 (a+1) = n) \\land Squarefree(a+1)$$$
Lean4
theorem sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) : ∃ a b : ℕ, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a := by
classical
set S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
have hSne : S.Nonempty := by
use 1
have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
simp [S, h1]
let s := Finset.max' S hSne
have hs : s ∈ S := Finset.max'_mem S hSne
simp only [S, Finset.mem_filter, Finset.mem_range] at hs
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
rw [hsa] at hn
obtain ⟨hlts, hlta⟩ := CanonicallyOrderedAdd.mul_pos.mp hn
rw [hsb] at hsa hn hlts
refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩
rintro x ⟨y, hy⟩
rw [Nat.isUnit_iff]
by_contra hx
refine Nat.lt_le_asymm ?_ (Finset.le_max' S ((b * x) ^ 2) ?_)
· convert
lt_mul_of_one_lt_right hlts
(one_lt_pow two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩)) using
1
rw [mul_pow]
· simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]
refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring
