-- 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:
case 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
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩

Result:
case 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
⊢ 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
s : ℕ := S.max' hSne
hs : s < n + 1 ∧ s ∣ n ∧ ∃ x, s = x ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs

Result:
case intro.intro.intro.intro
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 : ℕ
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
case 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 : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
obtain ⟨hlts, hlta⟩ := CanonicallyOrderedAdd.mul_pos.mp hn

Result:
case 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 : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
hlts : 0 < s
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
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 < b ^ 2 * a + 1 ∧ (b * x) ^ 2 ∣ b ^ 2 * a ∧ ∃ x_1, (b * x) ^ 2 = x_1 ^ 2

Tactic:
refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring

Result:
no goals

Proof state:
case intro.intro.intro.intro
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 : ℕ
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
rw [hsa] at hn

Result:
case 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 : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Proof state:
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

Tactic:
simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]

Result:
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 < b ^ 2 * a + 1 ∧ (b * x) ^ 2 ∣ b ^ 2 * a ∧ ∃ x_1, (b * x) ^ 2 = x_1 ^ 2

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
hs : s ∈ S
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
simp only [S, Finset.mem_filter, Finset.mem_range] at hs

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 < n + 1 ∧ s ∣ n ∧ ∃ x, s = x ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

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
⊢ IsUnit x

Tactic:
rw [Nat.isUnit_iff]

Result:
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
⊢ x = 1

Proof state:
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

Tactic:
have hSne : S.Nonempty := by
  use 1
  have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
  simp [S, h1]

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

Proof state:
case 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 : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
hlts : 0 < s
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
rw [hsb] at hsa hn hlts

Result:
case 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
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

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
⊢ x = 1

Tactic:
by_contra hx

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

Proof state:
case 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
⊢ Squarefree a

Tactic:
rintro x ⟨y, hy⟩

Result:
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
⊢ IsUnit x

Proof state:
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

Tactic:
rw [mul_pow]

Result:
no goals