awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
⊢ 0 < n ∧ ∃ (x : ℕ), 1 = HPow.hPow (β := ℕ) x 2

Tactic:
have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
h1 : 0 < n ∧ ∃ (x : ℕ), 1 = HPow.hPow (β := ℕ) x 2
⊢ 1 ∈ S

Tactic:
simp [S, h1]
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
⊢ S.Nonempty

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]
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
⊢ s ∈ S

Tactic:
have hs : s ∈ S := Finset.max'_mem S hSne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
hs : s ∈ S
⊢ s < n + 1 ∧ s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2

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

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
hs : s < n + 1 ∧ s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2
obtain :
  ∀ (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
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a

Tactic:
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hsa : n = s * a
b : ℕ
hsb : s = HPow.hPow (β := ℕ) b 2
rw :
  ∀ (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
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a

Tactic:
rw [hsa] at hn
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = HPow.hPow (β := ℕ) b 2
⊢ 0 < s

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

Premises used: Iff.mp, CanonicallyOrderedAdd.mul_pos
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = HPow.hPow (β := ℕ) b 2
hlts : 0 < s
⊢ 0 < a

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

Premises used: Iff.mp, CanonicallyOrderedAdd.mul_pos
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
⊢ 0 < HPow.hPow (β := ℕ) b 2 * a

Tactic:
rw [hsb] at hsa hn hlts
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
hn₁ : 0 < HPow.hPow (β := ℕ) b 2 * a
⊢ n = HPow.hPow (β := ℕ) b 2 * a

Tactic:
rw [hsb] at hsa hn hlts
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
hn₁ : 0 < HPow.hPow (β := ℕ) b 2 * a
hsa₁ : n = HPow.hPow (β := ℕ) b 2 * a
⊢ s = HPow.hPow (β := ℕ) b 2

Tactic:
rw [hsb] at hsa hn hlts
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
hn₁ : 0 < HPow.hPow (β := ℕ) b 2 * a
hsa₁ : n = HPow.hPow (β := ℕ) b 2 * a
hsb₁ : s = HPow.hPow (β := ℕ) b 2
⊢ 0 < HPow.hPow (β := ℕ) b 2

Tactic:
rw [hsb] at hsa hn hlts
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
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
⊢ 0 < a

Tactic:
rw [hsb] at hsa hn hlts
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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:
⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩

Premises used: two_ne_zero, And.intro, Exists.intro, Iff.mp, pow_pos_iff, Eq.symm
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
refine : Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a

Tactic:
refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
rw : x = 1
⊢ IsUnit x

Tactic:
rw [Nat.isUnit_iff]

Premises used: Nat.isUnit_iff
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
by_contra : ∀ (hx : ¬x = 1), False
⊢ x = 1

Tactic:
by_contra hx
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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

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

Premises used: HMul.hMul, HPow.hPow, Finset.le_max', Nat.lt_le_asymm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
refine_1 : S.max' ⋯ < HPow.hPow (β := ℕ) (b * x) 2
refine_2 : HPow.hPow (β := ℕ) (b * x) 2 ∈ S
⊢ False

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

Premises used: HMul.hMul, HPow.hPow, Finset.le_max', Nat.lt_le_asymm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
h : x = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
h : HPow.hPow (β := ℕ) (b * x) 2 = HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) x 2
⊢ S.max' ⋯ < HPow.hPow (β := ℕ) (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

Premises used: Iff.mpr, Nat.one_lt_pow, two_ne_zero, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, lt_mul_of_one_lt_right
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
h h₁ : HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) (b * x) 2 = HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) x 2

Tactic:
rw [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
refine_2 :
  HPow.hPow (β := ℕ) (b * x) 2 < HPow.hPow (β := ℕ) b 2 * a + 1 ∧
    HPow.hPow (β := ℕ) (b * x) 2 ∣ HPow.hPow (β := ℕ) b 2 * a ∧
      ∃ (x_1 : ℕ), HPow.hPow (β := ℕ) (b * x) 2 = HPow.hPow (β := ℕ) x_1 2
⊢ HPow.hPow (β := ℕ) (b * x) 2 ∈ S

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

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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 < HPow.hPow (β := ℕ) b 2 * a + 1 ∧
    HPow.hPow (β := ℕ) (b * x) 2 ∣ HPow.hPow (β := ℕ) b 2 * a ∧
      ∃ (x_1 : ℕ), HPow.hPow (β := ℕ) (b * x) 2 = HPow.hPow (β := ℕ) x_1 2

Tactic:
⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩

Premises used: Iff.mpr, HMul.hMul, Nat.lt_succ_iff, And.intro, Exists.intro, Nat.le_of_dvd, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
refine_2 refine_2₁ : HPow.hPow (β := ℕ) (b * x) 2 ∣ HPow.hPow (β := ℕ) b 2 * a
⊢ HPow.hPow (β := ℕ) (b * x) 2 < HPow.hPow (β := ℕ) b 2 * a + 1 ∧
    HPow.hPow (β := ℕ) (b * x) 2 ∣ HPow.hPow (β := ℕ) b 2 * a ∧
      ∃ (x_1 : ℕ), HPow.hPow (β := ℕ) (b * x) 2 = HPow.hPow (β := ℕ) x_1 2

Tactic:
refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
h : HPow.hPow (β := ℕ) b 2 * a = HPow.hPow (β := ℕ) (b * x) 2 * y
⊢ HPow.hPow (β := ℕ) (b * x) 2 ∣ HPow.hPow (β := ℕ) b 2 * a

Tactic:
use y
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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
h : HPow.hPow (β := ℕ) b 2 * (x * x * y) = HPow.hPow (β := ℕ) (b * x) 2 * y
⊢ HPow.hPow (β := ℕ) b 2 * a = HPow.hPow (β := ℕ) (b * x) 2 * y

Tactic:
rw [hy]
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2}
hSne : S.Nonempty
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 2 * (x * x * y) = HPow.hPow (β := ℕ) (b * x) 2 * y

Tactic:
ring
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h : 0 < n
obtain :
  ∀ (a₁ b₁ : ℕ) (ha₁ : 0 < a₁) (hb₁ : 0 < b₁) (hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n) (hab₂ : Squarefree a₁),
    ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h

Premises used: Nat.sq_mul_squarefree_of_pos
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
⟨a₁.pred, b₁.pred, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Nat.pred
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
refine_1 : HPow.hPow (β := ℕ) (b₁.pred + 1) 2 * (a₁.pred + 1) = n
refine_2 : Squarefree (a₁.pred + 1)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
refine ⟨a₁.pred, b₁.pred, ?_, ?_⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ HPow.hPow (β := ℕ) (b₁.pred + 1) 2 * (a₁.pred + 1) = n

Tactic:
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

Premises used: Nat.succ_pred_eq_of_pos, Nat.add_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ Squarefree (a₁.pred + 1)

Tactic:
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

Premises used: Nat.succ_pred_eq_of_pos, Nat.add_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
zero : ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = 0 ∧ Squarefree a
succ : ∀ (n : ℕ), ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
⊢ HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1 = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = 0 ∧ Squarefree a

Tactic:
exact ⟨1, 0, by simp, squarefree_one⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
succ :
  ∀ (a b : ℕ) (h₁ : HPow.hPow (β := ℕ) b 2 * a = n.succ) (h₂ : Squarefree a),
    ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a

Tactic:
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)

Premises used: Nat.sq_mul_squarefree_of_pos, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n a b : ℕ
h₁ : HPow.hPow (β := ℕ) b 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a

Tactic:
⟨a, b, h₁, h₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n a b : ℕ
h₁ : HPow.hPow (β := ℕ) b 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a

Tactic:
exact ⟨a, b, h₁, h₂⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Tactic:
simp [squarefree_mul_iff, Nat.coprime_iff_isRelPrime.mp hmn]

Premises used: squarefree_mul_iff, Iff.mp, Nat.coprime_iff_isRelPrime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
h : Squarefree (m * n)
⊢ m.Coprime n

Tactic:
coprime_of_dvd fun p hp hm hn => squarefree_iff_prime_squarefree.mp h p hp (mul_dvd_mul hm hn)

Premises used: Nat.coprime_of_dvd, mul_dvd_mul, Iff.mp, Nat.squarefree_iff_prime_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
rw : IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
rw₁ rw₂ : IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ IsRelPrime m n ∧ Squarefree m ∧ Squarefree n
⊢ Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n

Tactic:
rw [_root_.squarefree_mul_iff, Nat.coprime_iff_isRelPrime]

Premises used: squarefree_mul_iff, Nat.coprime_iff_isRelPrime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ Squarefree (m / m.gcd n * m.gcd n)

Tactic:
simpa [Nat.div_mul_cancel, gcd_dvd_left]

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).Coprime (m.gcd n)

Tactic:
have : Coprime (m / gcd m n) (gcd m n) :=
    coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
this : (m / m.gcd n).Coprime (m.gcd n)
⊢ (m / m.gcd n).Coprime n

Tactic:
simpa [Nat.div_mul_cancel, gcd_dvd_right] using
    (coprime_div_gcd_div_gcd (m := m) (gcd_ne_zero_right hn).bot_lt).mul_right this

Premises used: Nat.div_mul_cancel, Nat.Coprime.mul_right, Nat.coprime_div_gcd_div_gcd, Nat.gcd_dvd_right, Nat.gcd_ne_zero_right, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
rw : ∏ p ∈ n.primeFactorsList.toFinset, p = n
rw₁ : List.prod (List.map (fun (p : ℕ) ↦ p) n.primeFactorsList) = n
rw₂ : n.primeFactorsList.prod = n
rw₃ rw₄ : n = n
⊢ ∏ p ∈ n.primeFactors, p = n

Tactic:
rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]

Premises used: List.map_id', Nat.toFinset_factors, Squarefree.ne_zero, Squarefree.nodup_primeFactorsList, Nat.prod_primeFactorsList, List.prod_toFinset
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ Ne (α := ℕ) (∏ p ∈ s, p) 0

Tactic:
have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
h : ∀ (p : ℕ), p ∈ primeFactors (∏ p ∈ s, p) ↔ p ∈ s
⊢ primeFactors (∏ p ∈ s, p) = s

Tactic:
ext p
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
h : (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s
⊢ p ∈ primeFactors (∏ p ∈ s, p) ↔ p ∈ s

Tactic:
rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finsetProd_iff _)]

Premises used: Nat.mem_primeFactors_of_ne_zero, and_congr_right
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s

Tactic:
⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, dvd_rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
h : (Prime p ∧ ∃ a ∈ s, p ∣ a) → p ∈ s
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s

Tactic:
refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
h h₁ h₂ h₃ : q ∈ s
⊢ p ∈ s

Tactic:
rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]

Premises used: Nat.Prime.dvd_iff_eq, Nat.Prime.ne_one, Iff.mp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
h : ∀ (p : ℕ), p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

Tactic:
ext p
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ m / m.gcd n ≠ 0

Tactic:
simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]

Premises used: Squarefree.ne_zero, Nat.gcd_ne_zero_right, Ne.bot_lt, Nat.gcd_le_left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ m / m.gcd n ≠ 0

Tactic:
have : m / m.gcd n ≠ 0 := by simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
h : Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors

Tactic:
simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff,
    hm.ne_zero, hn, dvd_div_iff_mul_dvd (gcd_dvd_left _ _)]

Premises used: Nat.gcd_dvd_left, and_true, ne_eq, Finset.mem_sdiff, Squarefree.ne_zero, not_false_eq_true, Nat.dvd_div_iff_mul_dvd, not_and, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)

Tactic:
⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_isUnit <| hm _ <|
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩

Premises used: Nat.gcd_dvd_left, mul_dvd_mul_right, dvd_of_mul_left_dvd, Irreducible.not_isUnit, Nat.dvd_gcd, And.right, And.left, And.intro, Iff.intro, Nat.Coprime.mul_dvd_of_dvd_of_dvd, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
h : ∀ (hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)), (m.gcd n).Coprime p
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)

Tactic:
refine ⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_isUnit <| hm _ <|
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
h : ¬p ∣ m.gcd n
⊢ (m.gcd n).Coprime p

Tactic:
rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]

Premises used: Nat.coprime_comm, And.left, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n

Tactic:
fun hpn ↦ hp.2 hp.1.1 <| hpn.trans <| gcd_dvd_right _ _

Premises used: And.right, And.left, Nat.gcd_dvd_right, Not, Dvd.dvd.trans