awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
refine :
  (n + 2) / 2 * 2 + (n + 2) % 2 ≤
    1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
⊢ n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2

Tactic:
refine le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_

Premises used: Nat.div_add_mod', Nat.le_of_eq, HAdd.hAdd, OfNat.ofNat, Eq.symm, le_trans
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 = n + 2

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
rw : n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤
    1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2

Tactic:
rw [show (n + 2) / 2 * 2 + (n + 2) % 2 = n + 2 by grind]
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
simp :
  n + 2 ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) +
      HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * 2
⊢ n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2

Tactic:
simp only [shiftLeft_eq, Nat.one_mul]

Premises used: Nat.shiftLeft_eq, Nat.one_mul
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) +
      HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * 2

Tactic:
Nat.le_of_lt (Nat.le_trans lt_log2_self (le_add_right_of_le ?_))

Premises used: Nat.le_of_lt, Nat.le_trans, Nat.lt_log2_self, Nat.le_add_right_of_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
refine :
  HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1)
⊢ n + 2 ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) +
      HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * 2

Tactic:
refine Nat.le_of_lt (Nat.le_trans lt_log2_self (le_add_right_of_le ?_))

Premises used: Nat.le_of_lt, Nat.le_trans, Nat.lt_log2_self, Nat.le_add_right_of_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
rw : HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤ HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1 + ((n + 2).log2 / 2 + 1))
⊢ HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1)

Tactic:
rw [← Nat.pow_add]

Premises used: Nat.pow_add
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤ HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1 + ((n + 2).log2 / 2 + 1))

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n.IsSqrt n.sqrt

Tactic:
match n with
  | 0 => simp [IsSqrt, sqrt]
  | 1 => simp [IsSqrt, sqrt]
  | n + 2 =>
    have h : ¬ (n + 2) ≤ 1 := by simp
    simp only [IsSqrt, sqrt, h, ite_false]
    refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
    simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc]
    rw [Nat.lt_add_one_iff, Nat.add_assoc, ← Nat.mul_two]
    refine le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_
    rw [show (n + 2) / 2 * 2 + (n + 2) % 2 = n + 2 by grind]
    simp only [shiftLeft_eq, Nat.one_mul]
    refine Nat.le_of_lt (Nat.le_trans lt_log2_self (le_add_right_of_le ?_))
    rw [← Nat.pow_add]
    grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n.sqrt * n.sqrt ≤ n

Tactic:
(sqrt_isSqrt n).left

Premises used: _private.0.Nat.sqrt_isSqrt, And.left
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n.sqrt 2 ≤ n

Tactic:
simpa [Nat.pow_two] using sqrt_le n

Premises used: Nat.sqrt_le, Nat.pow_two
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n < n.sqrt.succ * n.sqrt.succ

Tactic:
(sqrt_isSqrt n).right

Premises used: _private.0.Nat.sqrt_isSqrt, And.right
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n < HPow.hPow (β := ℕ) n.sqrt.succ 2

Tactic:
simpa [Nat.pow_two] using lt_succ_sqrt n

Premises used: Nat.lt_succ_sqrt, Nat.pow_two
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
rw : n ≤ n.sqrt.succ * n.sqrt + n.sqrt
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
rw [← succ_mul]

Premises used: Nat.succ_mul
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt

Tactic:
le_of_lt_succ (lt_succ_sqrt n)

Premises used: Nat.lt_succ_sqrt, Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt

Tactic:
exact le_of_lt_succ (lt_succ_sqrt n)

Premises used: Nat.lt_succ_sqrt, Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
⊢ m ≤ n.sqrt ↔ m * m ≤ n

Tactic:
⟨fun h ↦ le_trans (mul_self_le_mul_self h) (sqrt_le n),
    fun h ↦ le_of_lt_succ <| Nat.mul_self_lt_mul_self_iff.1 <| lt_of_le_of_lt h (lt_succ_sqrt n)⟩

Premises used: lt_of_le_of_lt, Nat.mul_self_lt_mul_self_iff, Nat.mul_self_le_mul_self, Nat.sqrt_le, Nat.lt_succ_sqrt, Nat.le_of_lt_succ, Iff.intro, Iff.mp, le_trans
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
⊢ m ≤ n.sqrt ↔ HPow.hPow (β := ℕ) m 2 ≤ n

Tactic:
simpa only [Nat.pow_two] using le_sqrt

Premises used: Nat.pow_two, Nat.le_sqrt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
⊢ m.sqrt < n ↔ m < n * n

Tactic:
simp only [← not_le, le_sqrt]

Premises used: not_le, Nat.le_sqrt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
⊢ m.sqrt < n ↔ m < HPow.hPow (β := ℕ) n 2

Tactic:
simp only [← not_le, le_sqrt']

Premises used: not_le, Nat.le_sqrt'
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n.sqrt ≤ n

Tactic:
le_trans (le_mul_self _) (sqrt_le n)

Premises used: Nat.sqrt_le, Nat.le_mul_self, le_trans
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
h : m ≤ n
⊢ m.sqrt ≤ n.sqrt

Tactic:
le_sqrt.2 (le_trans (sqrt_le _) h)

Premises used: Iff.mpr, Nat.sqrt_le, Nat.le_sqrt, le_trans
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
⊢ sqrt 0 = 0

Tactic:
rfl

Premises used: Nat.sqrt, rfl, ite
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
⊢ sqrt 1 = 1

Tactic:
rfl

Premises used: Nat.sqrt, rfl, ite
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
h : n.sqrt = 0
this : n.sqrt < 1 ↔ n < HMul.hMul (α := ℕ) 1 1
⊢ n = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n = 0 → n.sqrt = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n a : ℕ
⊢ a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)

Tactic:
⟨fun e ↦ e.symm ▸ sqrt_isSqrt n,
   fun ⟨h₁, h₂⟩ ↦ le_antisymm (le_sqrt.2 h₁) (le_of_lt_succ <| sqrt_lt.2 h₂)⟩

Premises used: Iff.mpr, Nat.sqrt_lt, _private.0.Nat.sqrt_isSqrt, Eq.rec, Nat.sqrt, le_antisymm, Nat.le_of_lt_succ, Nat.le_sqrt, Iff.intro, Eq.symm, _private.0.Nat.eq_sqrt.match_1, Eq
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n a : ℕ
⊢ a = n.sqrt ↔ HPow.hPow (β := ℕ) a 2 ≤ n ∧ n < HPow.hPow (β := ℕ) (a + 1) 2

Tactic:
simpa only [Nat.pow_two] using eq_sqrt

Premises used: Nat.pow_two, Nat.eq_sqrt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
h : n.sqrt = 1
⊢ n.sqrt < 2

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
h : 1 < n
⊢ n * 1 < n * n

Tactic:
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ 0 < n.sqrt ↔ 0 < n

Tactic:
le_sqrt

Premises used: Nat.le_sqrt, Nat.lt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a n : ℕ
h : a ≤ n + n
⊢ n * n + a < n.succ * n.succ

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a n : ℕ
h : a ≤ n + n
⊢ n * n ≤ n * n + a

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a n : ℕ
h : a ≤ n + n
⊢ (HPow.hPow (β := ℕ) n 2 + a).sqrt = n

Tactic:
simpa [Nat.pow_two] using sqrt_add_eq n h

Premises used: Nat.pow_two, Nat.sqrt_add_eq
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ (n * n).sqrt = n

Tactic:
sqrt_add_eq n (zero_le _)

Premises used: Nat.zero_le, Nat.sqrt_add_eq
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ (HPow.hPow (β := ℕ) n 2).sqrt = n

Tactic:
sqrt_add_eq' n (zero_le _)

Premises used: Nat.zero_le, Nat.sqrt_add_eq'
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
this : n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
⊢ n.succ < n.sqrt.succ.succ * n.sqrt.succ.succ

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
⊢ log2 2 = 1

Tactic:
simp [log2_def]

Premises used: Nat.log2_def
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
⊢ sqrt 2 = 1

Tactic:
simp [sqrt, sqrt.iter]

Premises used: Nat.sqrt, Nat.sqrt.iter
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
hn : n ≠ 0
⊢ (succ 0 + 1).sqrt ≤ succ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
h : ∃ (n : ℕ), n * n = x
n : ℕ
hn : n * n = x
rw : (n * n).sqrt * (n * n).sqrt = n * n
rw₁ rw₂ : n * n = n * n
⊢ x.sqrt * x.sqrt = x

Tactic:
rw [← hn, sqrt_eq]

Premises used: Nat.sqrt_eq
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
⊢ (∃ (n : ℕ), HPow.hPow (β := ℕ) n 2 = x) ↔ HPow.hPow (β := ℕ) x.sqrt 2 = x

Tactic:
simpa only [Nat.pow_two] using exists_mul_self x

Premises used: Nat.exists_mul_self, Nat.pow_two
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n.sqrt * n.sqrt < n + 1

Tactic:
Nat.lt_succ_iff.mpr (sqrt_le _)

Premises used: Iff.mpr, Nat.sqrt_le, Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n.sqrt 2 < n + 1

Tactic:
Nat.lt_succ_iff.mpr (sqrt_le' _)

Premises used: Iff.mpr, Nat.sqrt_le', Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)

Tactic:
le_of_pred_lt (lt_succ_sqrt _)

Premises used: Nat.lt_succ_sqrt, Nat.le_of_pred_lt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ n + 1 ≤ HPow.hPow (β := ℕ) (n.sqrt + 1) 2

Tactic:
le_of_pred_lt (lt_succ_sqrt' _)

Premises used: Nat.lt_succ_sqrt', Nat.le_of_pred_lt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ m < t

Tactic:
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ t < m + 1

Tactic:
have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
m n : ℕ
⊢ HPow.hPow (β := ℕ) m 2 < n → n < HPow.hPow (β := ℕ) (m + 1) 2 → ¬∃ (t : ℕ), HPow.hPow (β := ℕ) t 2 = n

Tactic:
simpa only [Nat.pow_two] using not_exists_sq

Premises used: Nat.not_exists_sq, Nat.pow_two
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b c : ℕ
h : a = b * c
inl : ∀ (bc : b ≤ c), b ≤ a.sqrt ∨ c ≤ a.sqrt
inr : ∀ (cb : c ≤ b), b ≤ a.sqrt ∨ c ≤ a.sqrt
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
rcases le_total b c with bc | cb

Premises used: le_total
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b c : ℕ
h : a = b * c
bc : b ≤ c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc

Premises used: Iff.mpr, Eq.rec, Nat.mul_le_mul_left, Nat.le_sqrt, Or.inl, Eq.symm
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b c : ℕ
h : a = b * c
bc : b ≤ c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc

Premises used: Iff.mpr, Nat.le_sqrt, Or.inl
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

Premises used: Iff.mpr, Nat.mul_le_mul_right, Eq.rec, Nat.le_sqrt, Eq.symm, Or.inr
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
exact Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

Premises used: Iff.mpr, Nat.le_sqrt, Or.inr
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
rw : (↑n.primeFactorsList : Multiset ℕ).Nodup ↔ n.primeFactorsList.Nodup
⊢ Squarefree n ↔ n.primeFactorsList.Nodup

Tactic:
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]

Premises used: Nat.factors_eq, UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList : Multiset ℕ).Nodup ↔ n.primeFactorsList.Nodup

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
⊢ n.primeFactorsList.Nodup

Tactic:
(Nat.squarefree_iff_nodup_primeFactorsList hn.ne_zero).mp hn

Premises used: Nat.squarefree_iff_nodup_primeFactorsList, Squarefree.ne_zero, Iff.mp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
⊢ Squarefree n ↔ ∀ (x : ℕ), Prime x → ¬x * x ∣ n

Tactic:
squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible ⟨_, prime_two⟩

Premises used: Nat.Prime, squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible, Nat.prime_two, Exists.intro
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : Squarefree n
inl : ∀ (hn : Squarefree (R := ℕ) 0), LE.le (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
inr : ∀ (hn' : n ≠ 0), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
p : ℕ
hn : Squarefree (R := ℕ) 0
⊢ LE.le (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x

Tactic:
rw [squarefree_iff_emultiplicity_le_one] at hn

Premises used: squarefree_iff_emultiplicity_le_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
hn₁ : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
⊢ n ≠ 0

Tactic:
rw [squarefree_iff_emultiplicity_le_one] at hn

Premises used: squarefree_iff_emultiplicity_le_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
pos : ∀ (hp : Prime p), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
neg : ∀ (hp : ¬Prime p), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
by_cases hp : p.Prime

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ emultiplicity p n ≤ 1 ∨ IsUnit p

Tactic:
have := hn p
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
pos : multiplicity p n ≤ 1
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
rw [← multiplicity_eq_factorization hp hn']

Premises used: Nat.multiplicity_eq_factorization
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ emultiplicity p n ≤ 1

Tactic:
simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this

Premises used: Nat.isUnit_iff, Nat.Prime.ne_one, or_false
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1
⊢ multiplicity p n ≤ 1

Tactic:
multiplicity_le_of_emultiplicity_le this

Premises used: multiplicity_le_of_emultiplicity_le
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1
⊢ multiplicity p n ≤ 1

Tactic:
exact multiplicity_le_of_emultiplicity_le this

Premises used: multiplicity_le_of_emultiplicity_le
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
neg : LE.le (α := ℕ) 0 1
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
rw [factorization_eq_zero_of_not_prime _ hp]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ LE.le (α := ℕ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ LE.le (α := ℕ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n p : ℕ
hn : Squarefree n
hp : Prime p
hpn : p ∣ n
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
(hn.natFactorization_le_one _).antisymm <| (hp.dvd_iff_one_le_factorization hn.ne_zero).1 hpn

Premises used: LE.le.antisymm, Nat.Prime.dvd_iff_one_le_factorization, Squarefree.natFactorization_le_one, Squarefree.ne_zero, Iff.mp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
rw : ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1
⊢ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]

Premises used: Nat.squarefree_iff_nodup_primeFactorsList, List.nodup_iff_count_le_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
a : ℕ
rw : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) a : ℕ) (1 : ℕ)
⊢ List.count a n.primeFactorsList ≤ 1

Tactic:
rw [primeFactorsList_count_eq]

Premises used: Nat.primeFactorsList_count_eq
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
a : ℕ
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) a : ℕ) (1 : ℕ)

Tactic:
apply hn'
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : n ≠ 0
⊢ Squarefree n ↔ ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
⟨fun hn => hn.natFactorization_le_one, squarefree_of_factorization_le_one hn⟩

Premises used: Nat.squarefree_of_factorization_le_one, Squarefree.natFactorization_le_one, Iff.intro
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
refine :
  ∀ (h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)) (p : ℕ),
    Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

Tactic:
refine ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => ?_⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
pos : ∀ (hp : Prime p), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
neg : ∀ (hp : ¬Prime p), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
by_cases hp : p.Prime

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ p ∣ n ↔ p ∣ m

Tactic:
have h₁ := h _ hp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : p ∣ n ↔ p ∣ m
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔
    Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff,
      hp.dvd_iff_one_le_factorization hm.ne_zero, not_le, lt_one_iff] at h₁

Premises used: not_le, not_iff_not, Nat.Prime.dvd_iff_one_le_factorization, Squarefree.ne_zero, Nat.lt_one_iff
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ :
  Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔
    Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
have h₂ := hn.natFactorization_le_one p
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ :
  Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔
    Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h₂ : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ LE.le (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
have h₃ := hm.natFactorization_le_one p
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ :
  Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔
    Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
h₂ : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
h₃ : LE.le (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
neg : Eq (α := ℕ) (0 : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_eq_zero_of_not_prime _ hp, factorization_eq_zero_of_not_prime _ hp]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn_1 : n ≠ 1
hn : Squarefree n
hk : Ne (α := ℕ) 1 0
⊢ Squarefree (HPow.hPow (β := ℕ) n 1)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
refine : ∀ (h : Squarefree (n ^ k)), Squarefree n ∧ k = 1
⊢ Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1

Tactic:
refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
inl : ∀ (hn : Ne (α := ℕ) 0 1) (h : Squarefree (HPow.hPow (α := ℕ) 0 k)), Squarefree (R := ℕ) 0 ∧ k = 1
inr : Squarefree n ∧ k = 1
⊢ Squarefree n ∧ k = 1

Tactic:
rcases eq_or_ne n 0 with (rfl | -)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
k : ℕ
hk : k ≠ 0
hn : Ne (α := ℕ) 0 1
h : Squarefree (HPow.hPow (α := ℕ) 0 k)
⊢ Squarefree (R := ℕ) 0 ∧ k = 1

Tactic:
simp [zero_pow hk] at h

Premises used: zero_pow
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Tactic:
⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩

Premises used: Squarefree.squarefree_of_dvd, dvd_pow_self, And.intro, by_contradiction
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
inr : ∀ (h₁ : ¬k = 1), False
⊢ Squarefree n ∧ k = 1

Tactic:
refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ 2 ≤ k

Tactic:
have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
apply : n * n ∣ n ^ k
⊢ False

Tactic:
apply hn (Nat.isUnit_iff.1 (h _ _))

Premises used: Nat.isUnit_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
rw : HPow.hPow (β := ℕ) n 2 ∣ n ^ k
⊢ n * n ∣ n ^ k

Tactic:
rw [← sq]

Premises used: sq
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ HPow.hPow (β := ℕ) n 2 ∣ n ^ k

Tactic:
pow_dvd_pow _ this

Premises used: pow_dvd_pow
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ HPow.hPow (β := ℕ) n 2 ∣ n ^ k

Tactic:
exact pow_dvd_pow _ this

Premises used: pow_dvd_pow