-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
set set₁ : ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₂ set₃ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty), ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₄ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (hs : s ∈ S), ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₅ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (hs : s < n + 1 ∧ s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₆ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a : ℕ) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₇ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a : ℕ) (hn : 0 < s * a) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₈ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a : ℕ) (hn : 0 < s * a) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < s)
      (hlta : 0 < a), ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₉ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₁₀ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a), Squarefree a
set₁₁ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a) (x y : ℕ)
      (hy : a = x * x * y), IsUnit x
set₁₂ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a) (x y : ℕ)
      (hy : a = x * x * y), x = 1
set₁₃ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a) (x y : ℕ)
      (hy : a = x * x * y) (hx : ¬x = 1), False
refine_1 :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a) (x y : ℕ)
      (hy : a = x * x * y) (hx : ¬x = 1), S.max' ⋯ < HPow.hPow (β := ℕ) (b * x) 2
refine_2 refine_2₁ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a b : ℕ) (hn : 0 < HPow.hPow (β := ℕ) b 2 * a) (hsa : n = HPow.hPow (β := ℕ) b 2 * a)
      (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < HPow.hPow (β := ℕ) b 2) (hlta : 0 < a) (x y : ℕ)
      (hy : a = x * x * y) (hx : ¬x = 1), HPow.hPow (β := ℕ) (b * x) 2 ∈ S
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a

Tactic:
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

Premises used: Finset.mem_range, Finset.range, Nat.isUnit_iff, HAdd.hAdd, Iff.mp, Finset.mem_filter, CanonicallyOrderedAdd.mul_pos, OfNat.ofNat, mul_pow