awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n

Tactic:
⟨?_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩

Premises used: Irreducible.squarefree, And.intro, Iff.intro, Nat.Prime.isPrimePow
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
refine : Squarefree n ∧ IsPrimePow n → Prime n
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n

Tactic:
refine ⟨?_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
rw : (Squarefree n ∧ ∃ (p : ℕ) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
⊢ Squarefree n ∧ IsPrimePow n → Prime n

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Squarefree p ∧ k = 1

Tactic:
rw [squarefree_pow_iff hp.ne_one hk.ne'] at h

Premises used: Nat.squarefree_pow_iff, LT.lt.ne', Nat.Prime.ne_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
rwa : Prime (HPow.hPow (β := ℕ) p 1)
rwa₁ rwa₂ rwa₃ rwa₄ : Prime p
⊢ Prime (p ^ k)

Tactic:
rwa [h.2, pow_one]

Premises used: And.right, pow_one
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
m n_1 p n k : ℕ
h : ¬n < k * k
⊢ n.sqrt - k < n.sqrt + 2 - k

Tactic:
Nat.minFac_lemma n k h

Premises used: Nat.minFac_lemma
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
m n_1 p n k : ℕ
h : ¬n < k * k
⊢ n.sqrt - k < n.sqrt + 2 - k

Tactic:
exact Nat.minFac_lemma n k h

Premises used: Nat.minFac_lemma
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
m n_1 p n k : ℕ
h : ¬n < k * k
this : n.sqrt - k < n.sqrt + 2 - k
n' : ℕ := n / k
h₁ : n' ≤ n
⊢ n'.sqrt - k ≤ n.sqrt - k

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
s : Finset ℕ
m n_1 p n k : ℕ
h : ¬n < k * k
this : n.sqrt - k < n.sqrt + 2 - k
n' : ℕ := n / k
⊢ n' ≤ n

Tactic:
apply div_le_self

Premises used: Nat.div_le_self
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
p : ℕ
pp : Prime p
dp : p * p ∣ n
e : k = p
⊢ Prime k

Tactic:
subst e
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
p : ℕ
pp : Prime p
dp : p * p ∣ n
e : k = p
pp₁ : Prime k
⊢ k * k ∣ n

Tactic:
subst e
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
pp : Prime k
dp : k * k ∣ n
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
⊢ ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n

Tactic:
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
    have :=
      (coprime_primes pk pp).2 fun e => by
        subst e
        contradiction
    (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
none : ∀ (H : (n / k).MinSqFacProp Option.none), n.MinSqFacProp Option.none
some : ∀ (d : ℕ) (H : (n / k).MinSqFacProp (Option.some d)), n.MinSqFacProp (Option.some d)
⊢ n.MinSqFacProp o

Tactic:
rcases o with - | d
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : (n / k).MinSqFacProp Option.none
none : ∀ (H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k) (x : ℕ), Prime x → ¬x * x ∣ n
⊢ n.MinSqFacProp Option.none

Tactic:
rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢

Premises used: Nat.MinSqFacProp, Nat.squarefree_iff_prime_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
⊢ ∀ (x : ℕ), Prime x → ¬x * x ∣ n

Tactic:
fun p pp dp => H p pp ((dvd_div_iff_mul_dvd dk).2 (this _ pp dp))

Premises used: Iff.mpr, Nat.dvd_div_iff_mul_dvd, Not
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
⊢ ∀ (x : ℕ), Prime x → ¬x * x ∣ n

Tactic:
exact fun p pp dp => H p pp ((dvd_div_iff_mul_dvd dk).2 (this _ pp dp))

Premises used: Iff.mpr, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : (n / k).MinSqFacProp (some d)
⊢ Prime d

Tactic:
obtain ⟨H1, H2, H3⟩ := H
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : (n / k).MinSqFacProp (some d)
H1 : Prime d
⊢ d * d ∣ n / k

Tactic:
obtain ⟨H1, H2, H3⟩ := H
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : (n / k).MinSqFacProp (some d)
H1 : Prime d
H2 : d * d ∣ n / k
⊢ ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p

Tactic:
obtain ⟨H1, H2, H3⟩ := H
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : d * d ∣ n / k
H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ k * (d * d) ∣ n

Tactic:
simp only [dvd_div_iff_mul_dvd dk] at H2 H3

Premises used: Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : d * d ∣ n / k
H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
H2₁ : k * (d * d) ∣ n
⊢ ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p

Tactic:
simp only [dvd_div_iff_mul_dvd dk] at H2 H3

Premises used: Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ n.MinSqFacProp (some d)

Tactic:
⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩

Premises used: dvd_trans, dvd_mul_left, Nat.MinSqFacProp, And.intro
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ n.MinSqFacProp (some d)

Tactic:
exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
rw :
  n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
⊢ n.MinSqFacProp (n.minSqFacAux k)

Tactic:
rw [minSqFacAux]

Premises used: Nat.minSqFacAux
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
pos :
  ∀ (h : n < k * k),
    n.MinSqFacProp
      (if h : n < k * k then none
      else
        have this := ⋯;
        if k ∣ n then
          let n' := n / k;
          have this := ⋯;
          if k ∣ n' then some k else n'.minSqFacAux (k + 2)
        else n.minSqFacAux (k + 2))
neg :
  ∀ (h : ¬n < k * k),
    n.MinSqFacProp
      (if h : n < k * k then none
      else
        have this := ⋯;
        if k ∣ n then
          let n' := n / k;
          have this := ⋯;
          if k ∣ n' then some k else n'.minSqFacAux (k + 2)
        else n.minSqFacAux (k + 2))
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
by_cases h : n < k * k
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
pos : n.MinSqFacProp none
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
simp only [h, ↓reduceDIte]

Premises used: reduceDIte
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
neg :
  n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
simp only [h, ↓reduceDIte]

Premises used: reduceDIte
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp none

Tactic:
squarefree_iff_prime_squarefree.2 fun p pp d => ?_

Premises used: Iff.mpr, Nat.MinSqFacProp, Nat.squarefree_iff_prime_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
pos : ∀ (p : ℕ) (pp : Prime p) (d : p * p ∣ n), False
⊢ n.MinSqFacProp none

Tactic:
refine squarefree_iff_prime_squarefree.2 fun p pp d => ?_

Premises used: Iff.mpr, Nat.squarefree_iff_prime_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
⊢ k ≤ p

Tactic:
have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this : k ≤ p
⊢ k * k ≤ p * p

Tactic:
have := Nat.mul_le_mul this this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this_1 : k ≤ p
this : k * k ≤ p * p
⊢ False

Tactic:
not_le_of_gt h (le_trans this (le_of_dvd n0 d))

Premises used: not_le_of_gt, Nat.le_of_dvd, le_trans
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this_1 : k ≤ p
this : k * k ≤ p * p
⊢ False

Tactic:
exact not_le_of_gt h (le_trans this (le_of_dvd n0 d))

Premises used: not_le_of_gt, Nat.le_of_dvd, le_trans
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
lia
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
have k2 : 2 ≤ k := by lia
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ 0 < k

Tactic:
have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ n' ≤ n

Tactic:
have hn' := le_of_dvd n0 nd'
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ n'.sqrt - k ≤ n.sqrt - k

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3

Tactic:
simp [e, left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
have : ∀ (this : n'.sqrt - k < n.sqrt + 2 - k) (m : ℕ) (m2 : Prime m) (d : m ∣ n'), k + 2 ≤ m
⊢ n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
refine
      have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
        lt_of_le_of_lt (by gcongr) (Nat.minFac_lemma n k h)
      @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
        (by simp [e, left_distrib]) fun m m2 d => ?_

Premises used: lt_of_le_of_lt, Nat.minFac_lemma, HAdd.hAdd, Nat.pos_of_dvd_of_pos, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
inl : ∀ (m2 : Prime k) (d : k ∣ n'), k + 2 ≤ k
inr : ∀ (ml : k < m), k + 2 ≤ m
⊢ k + 2 ≤ m

Tactic:
rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with rfl | ml

Premises used: dvd_trans, Nat.eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m2 : Prime k
d : k ∣ n'
⊢ k + 2 ≤ k

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
inr : ¬k.succ = m
⊢ k + 2 ≤ m

Tactic:
apply (Nat.eq_or_lt_of_le ml).resolve_left

Premises used: Or.resolve_left, Nat.eq_or_lt_of_le
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : k.succ = m
⊢ (2 * i + 3).succ ∣ n'

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : k.succ = m
d₁ : (2 * i + 3).succ ∣ n'
⊢ k < m

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : k.succ = m
d₁ : (2 * i + 3).succ ∣ n'
ml₁ : k < m
⊢ k.succ = m

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : (2 * i + 3).succ ∣ n'
ml : k < m
me : k.succ = m
⊢ 2 * (i + 2) ∣ n'

Tactic:
change 2 * (i + 2) ∣ n' at d

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
⊢ k ≤ 2

Tactic:
have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this_1 : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : k ≤ 2
⊢ 2 * i + 3 ≤ 2

Tactic:
rw [e] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this_1 : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2

Tactic:
lia
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this_1 : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False

Tactic:
exact absurd this (by lia)

Premises used: absurd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
⊢ ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by
    intro n' nd' nk
    have hn' := le_of_dvd n0 nd'
    refine
      have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
        lt_of_le_of_lt (by gcongr) (Nat.minFac_lemma n k h)
      @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
        (by simp [e, left_distrib]) fun m m2 d => ?_
    rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with rfl | ml
    · contradiction
    apply (Nat.eq_or_lt_of_le ml).resolve_left
    intro me
    rw [← me, e] at d
    change 2 * (i + 2) ∣ n' at d
    have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
    rw [e] at this
    exact absurd this (by lia)
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
⊢ k ∣ n → Prime k

Tactic:
fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩

Premises used: Iff.mpr, Nat.minFac_le, le_antisymm, And.intro, Nat.prime_def_minFac
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
refine : ∀ (dk : k ∣ n), k ≤ k.minFac
⊢ k ∣ n → Prime k

Tactic:
refine fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩

Premises used: Iff.mpr, Nat.minFac_le, le_antisymm, And.intro, Nat.prime_def_minFac
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
dk : k ∣ n
⊢ k ≤ k.minFac

Tactic:
ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)

Premises used: Nat.minFac_dvd, dvd_trans, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
dk : k ∣ n
⊢ k ≤ k.minFac

Tactic:
exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)

Premises used: Nat.minFac_dvd, dvd_trans, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
⊢ k ∣ n → Prime k

Tactic:
have pk : k ∣ n → Prime k := by
    refine fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩
    exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
pos : ∀ (dk : k ∣ n) (dkk : k ∣ n / k), n.MinSqFacProp (some k)
neg : ∀ (dk : k ∣ n) (dkk : ¬k ∣ n / k), n.MinSqFacProp ((n / k).minSqFacAux (k + 2))
neg₁ : ∀ (dk : ¬k ∣ n), n.MinSqFacProp (n.minSqFacAux (k + 2))
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))

Tactic:
split_ifs with dk dkk
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ n.MinSqFacProp (some k)

Tactic:
⟨pk dk, (Nat.dvd_div_iff_mul_dvd dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩

Premises used: dvd_trans, Nat.MinSqFacProp, And.intro, Exists.intro, Iff.mp, Nat.dvd_div_iff_mul_dvd, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ n.MinSqFacProp (some k)

Tactic:
exact ⟨pk dk, (Nat.dvd_div_iff_mul_dvd dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ (n / k).MinSqFacProp ((n / k).minSqFacAux (k + 2))

Tactic:
specialize IH (n / k) (div_dvd_of_dvd dk) dkk

Premises used: HDiv.hDiv, Nat.div_dvd_of_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
IH : (n / k).MinSqFacProp ((n / k).minSqFacAux (k + 2))
⊢ n.MinSqFacProp ((n / k).minSqFacAux (k + 2))

Tactic:
minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff_mul_dvd dk).2 dkk) IH

Premises used: Iff.mpr, mt, Nat.minSqFacProp_div, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
IH : (n / k).MinSqFacProp ((n / k).minSqFacAux (k + 2))
⊢ n.MinSqFacProp ((n / k).minSqFacAux (k + 2))

Tactic:
exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff_mul_dvd dk).2 dkk) IH

Premises used: Iff.mpr, mt, Nat.minSqFacProp_div, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux (k + 2))

Tactic:
IH n (dvd_refl _) dk

Premises used: dvd_refl