awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n_1 n : ℕ
h : ¬n + 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)
have rw : HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤ HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1 + ((n + 2).log2 / 2 + 1))
Tactic: rw [← Nat.pow_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
have rw : n ≤ n.sqrt.succ * n.sqrt + n.sqrt
Tactic: rw [← succ_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (hypothesis)
Goal:
n : ℕ
h : 1 < n
⊢ n < n * n
have this : n * 1 < n * n
Tactic: have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
x : ℕ
h : ∃ (n : ℕ), n * n = x
n : ℕ
hn : n * n = x
⊢ x.sqrt * x.sqrt = x
have rw : (n * n).sqrt * (n * n).sqrt = n * n
Tactic: rw [← hn, sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
x : ℕ
h : ∃ (n : ℕ), n * n = x
n : ℕ
hn : n * n = x
rw : (n * n).sqrt * (n * n).sqrt = n * n
⊢ x.sqrt * x.sqrt = x
have rw₁ : n * n = n * n
Tactic: rw [← hn, sqrt_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (hypothesis)
Goal:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
have h1 : m < t
Tactic: have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (hypothesis)
Goal:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
have h2 : t < m + 1
Tactic: have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
a b c : ℕ
h : a = b * c
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt
have inl : ∀ (bc : b ≤ c), b ≤ a.sqrt ∨ c ≤ a.sqrt
Tactic: rcases le_total b c with bc | cb
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
a b c : ℕ
h : a = b * c
inl : ∀ (bc : b ≤ c), b ≤ a.sqrt ∨ c ≤ a.sqrt
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt
have inr : ∀ (cb : c ≤ b), b ≤ a.sqrt ∨ c ≤ a.sqrt
Tactic: rcases le_total b c with bc | cb
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
⊢ Squarefree n ↔ n.primeFactorsList.Nodup
have rw : (↑n.primeFactorsList : Multiset ℕ).Nodup ↔ n.primeFactorsList.Nodup
Tactic: rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n p : ℕ
hn : Squarefree n
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have inl : ∀ (hn : Squarefree (R := ℕ) 0), LE.le (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: rcases eq_or_ne n 0 with (rfl | hn')
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n p : ℕ
hn : Squarefree n
inl : ∀ (hn : Squarefree (R := ℕ) 0), LE.le (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have inr : ∀ (hn' : n ≠ 0), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: rcases eq_or_ne n 0 with (rfl | hn')
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have hn₁ : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
Tactic: rw [squarefree_iff_emultiplicity_le_one] at hn
Cleared hypotheses: hn, hn'
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have pos : ∀ (hp : Prime p), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: by_cases hp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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 : ℕ)
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have neg : ∀ (hp : ¬Prime p), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: by_cases hp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have this : emultiplicity p n ≤ 1 ∨ IsUnit p
Tactic: have := hn p
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have pos : multiplicity p n ≤ 1
Tactic: rw [← multiplicity_eq_factorization hp hn']
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ multiplicity p n ≤ 1
have this₁ : emultiplicity p n ≤ 1
Tactic: simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have neg : LE.le (α := ℕ) 0 1
Tactic: rw [factorization_eq_zero_of_not_prime _ hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ Squarefree n
have rw : ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1
Tactic: rw [squarefree_iff_nodup_primeFactorsList hn, List.nodup_iff_count_le_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
a : ℕ
⊢ List.count a n.primeFactorsList ≤ 1
have rw : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) a : ℕ) (1 : ℕ)
Tactic: rw [primeFactorsList_count_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
have refine : ∀ (h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)) (p : ℕ),
  Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : ∀ (hp : Prime p), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: by_cases hp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : ∀ (hp : ¬Prime p), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: by_cases hp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have h₁ : p ∣ n ↔ p ∣ m
Tactic: have h₁ := h _ hp
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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 : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have h₂ : 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₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have h₂ : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: have h₂ := hn.natFactorization_le_one p
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have h₃ : LE.le (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: have h₃ := hm.natFactorization_le_one p
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : Eq (α := ℕ) (0 : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorization_eq_zero_of_not_prime _ hp, factorization_eq_zero_of_not_prime _ hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [factorization_eq_zero_of_not_prime _ hp, factorization_eq_zero_of_not_prime _ hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1
have refine : ∀ (h : Squarefree (n ^ k)), Squarefree n ∧ k = 1
Tactic: refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
have inl : ∀ (hn : Ne (α := ℕ) 0 1) (h : Squarefree (HPow.hPow (α := ℕ) 0 k)), Squarefree (R := ℕ) 0 ∧ k = 1
Tactic: rcases eq_or_ne n 0 with (rfl | -)
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
have inr : ∀ (h₁ : ¬k = 1), False
Tactic: refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ False
have this : 2 ≤ k
Tactic: have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ False
have apply : n * n ∣ n ^ k
Tactic: apply hn (Nat.isUnit_iff.1 (h _ _))
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n * n ∣ n ^ k
have rw : HPow.hPow (β := ℕ) n 2 ∣ n ^ k
Tactic: rw [← sq]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n
have refine : Squarefree n ∧ IsPrimePow n → Prime n
Tactic: refine ⟨?_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n
have rw : (Squarefree n ∧ ∃ (p : ℕ) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
Tactic: rw [isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)
have h₁ : Squarefree p ∧ k = 1
Tactic: rw [squarefree_pow_iff hp.ne_one hk.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
have rwa : Prime (HPow.hPow (β := ℕ) p 1)
Tactic: rwa [h.2, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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'.sqrt - k ≤ n.sqrt - k
have h₁ : n' ≤ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ False
have dp₁ : k * k ∣ n
Tactic: subst e
Cleared hypotheses: p, pp, dp, e
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
⊢ n.MinSqFacProp o
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
⊢ n.MinSqFacProp o
have none : ∀ (H : (n / k).MinSqFacProp none), n.MinSqFacProp none
Tactic: rcases o with - | d
Cleared hypotheses: o, H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
⊢ n.MinSqFacProp o
have some : ∀ (d : ℕ) (H : (n / k).MinSqFacProp (some d)), n.MinSqFacProp (some d)
Tactic: rcases o with - | d
Cleared hypotheses: o, H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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 none
⊢ n.MinSqFacProp none
have none : ∀ (H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k) (x : ℕ), Prime x → ¬x * x ∣ n
Tactic: rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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)
⊢ n.MinSqFacProp (some d)
have H1 : Prime d
Tactic: obtain ⟨H1, H2, H3⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ n.MinSqFacProp (some d)
have H2 : d * d ∣ n / k
Tactic: obtain ⟨H1, H2, H3⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ n.MinSqFacProp (some d)
have H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
Tactic: obtain ⟨H1, H2, H3⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ n.MinSqFacProp (some d)
have H2₁ : k * (d * d) ∣ n
Tactic: simp only [dvd_div_iff_mul_dvd dk] at H2 H3
Cleared hypotheses: H2, H3
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ n.MinSqFacProp (some d)
have H3₁ : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
Tactic: simp only [dvd_div_iff_mul_dvd dk] at H2 H3
Cleared hypotheses: H2, H3
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ n.MinSqFacProp (n.minSqFacAux k)
have rw : n.MinSqFacProp
  (if h : n < k * k then none
  else
    have this := sorry;
    if k ∣ n then
      let n' := n / k;
      have this := sorry;
      if k ∣ n' then some k else n'.minSqFacAux (k + 2)
    else n.minSqFacAux (k + 2))
Tactic: rw [minSqFacAux]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ 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))
have pos : ∀ (h : n < k * k),
  n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := sorry;
      if k ∣ n then
        let n' := n / k;
        have this := sorry;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
Tactic: by_cases h : n < k * k
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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))
⊢ 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))
have neg : ∀ (h : ¬n < k * k),
  n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := sorry;
      if k ∣ n then
        let n' := n / k;
        have this := sorry;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
Tactic: by_cases h : n < k * k
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
    (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))
have pos : n.MinSqFacProp none
Tactic: simp only [h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
    (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))
have 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))
Tactic: simp only [h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
have pos : ∀ (p : ℕ) (pp : Prime p) (d : p * p ∣ n), False
Tactic: refine squarefree_iff_prime_squarefree.2 fun p pp d => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ False
have this : k ≤ p
Tactic: have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ False
have this₁ : k * k ≤ p * p
Tactic: have := Nat.mul_le_mul this this
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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 (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
have k2 : 2 ≤ k
Tactic: have k2 : 2 ≤ k := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
have k0 : 0 < k
Tactic: have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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'.MinSqFacProp (n'.minSqFacAux (k + 2))
have hn' : n' ≤ n
Tactic: have hn' := le_of_dvd n0 nd'
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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'.MinSqFacProp (n'.minSqFacAux (k + 2))
have have : ∀ (this : n'.sqrt - k < n.sqrt + 2 - k) (m : ℕ) (m2 : Prime m) (d : m ∣ n'), k + 2 ≤ m
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 => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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'
⊢ k + 2 ≤ m
have inl : ∀ (m2 : Prime k) (d : k ∣ n'), k + 2 ≤ k
Tactic: rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with rfl | ml
Cleared hypotheses: m, m2, d
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
⊢ k + 2 ≤ m
have inr : ∀ (ml : k < m), k + 2 ≤ m
Tactic: rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with rfl | ml
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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
⊢ k + 2 ≤ m
have inr : ¬k.succ = m
Tactic: apply (Nat.eq_or_lt_of_le ml).resolve_left
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
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
⊢ False
have d₁ : (2 * i + 3).succ ∣ n'
Tactic: rw [← me, e] at d
Cleared hypotheses: d, ml, me