-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
have 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
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
Cleared hypotheses: hn