-- Mathlib/Data/Nat/Squarefree.lean
theorem sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) :
    ∃ a b : ℕ, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
let s := Finset.max' S hSne

Result:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
n : ℕ
hn : 0 < n
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
set S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}

Result:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
h1 : 0 < n ∧ ∃ x, 1 = x ^ 2
⊢ 1 ∈ S

Tactic:
simp [S, h1]

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
⊢ S.Nonempty

Tactic:
use 1

Result:
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
⊢ 1 ∈ S

Proof state:
case intro.intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ False

Tactic:
refine Nat.lt_le_asymm ?_ (Finset.le_max' S ((b * x) ^ 2) ?_)

Result:
case intro.intro.intro.intro.intro.intro.refine_1
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ S.max' ⋯ < (b * x) ^ 2

case intro.intro.intro.intro.intro.intro.refine_2
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∈ S

Proof state:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
have hs : s ∈ S := Finset.max'_mem S hSne

Result:
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
hs : s ∈ S
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ S.max' ⋯ < (b * x) ^ 2

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

Result:
case h.e'_4
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 = b ^ 2 * x ^ 2

Proof state:
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
⊢ 1 ∈ S

Tactic:
have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩

Result:
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
h1 : 0 < n ∧ ∃ x, 1 = x ^ 2
⊢ 1 ∈ S

Proof state:
n : ℕ
S : Finset ℕ := filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (range (n + 1))
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
h : x = 0
⊢ False

Tactic:
simp_all

Result:
no goals