awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (2 * i + 3).succ ∣ n'
ml : k < m
me : k.succ = m
⊢ False
have d₁ : 2 * (i + 2) ∣ n'
Tactic: change 2 * (i + 2) ∣ n' at d
Cleared hypotheses: 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
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'
⊢ False
have this₁ : k ≤ 2
Tactic: have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
-- 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_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
⊢ False
have this₁ : 2 * i + 3 ≤ 2
Tactic: rw [e] at this
Cleared hypotheses: 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
k2 : 2 ≤ k
k0 : 0 < 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 IH : ∀ (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)
-- 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
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
⊢ k ∣ n → Prime k
have refine : ∀ (dk : k ∣ n), k ≤ k.minFac
Tactic: refine fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩
-- 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
IH : ∀ (n' : ℕ), n' ∣ n → ¬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))
have pk : 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)
-- 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
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime 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 pos : ∀ (dk : k ∣ n) (dkk : k ∣ n / k), n.MinSqFacProp (some k)
Tactic: split_ifs with dk dkk
-- 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
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)
⊢ 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 neg : ∀ (dk : k ∣ n) (dkk : ¬k ∣ n / k), n.MinSqFacProp ((n / k).minSqFacAux (k + 2))
Tactic: split_ifs with dk dkk
-- 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
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))
⊢ 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 neg₁ : ∀ (dk : ¬k ∣ n), n.MinSqFacProp (n.minSqFacAux (k + 2))
Tactic: split_ifs with dk dkk
-- 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
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 ((n / k).minSqFacAux (k + 2))
have IH₁ : (n / k).MinSqFacProp ((n / k).minSqFacAux (k + 2))
Tactic: specialize IH (n / k) (div_dvd_of_dvd dk) dkk
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)
have pos : ∀ (d2 : 2 ∣ n) (d4 : 2 ∣ n / 2), n.MinSqFacProp (some 2)
Tactic: split_ifs with d2 d4
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
pos : ∀ (d2 : 2 ∣ n) (d4 : 2 ∣ n / 2), n.MinSqFacProp (some 2)
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)
have neg : ∀ (d2 : 2 ∣ n) (d4 : ¬2 ∣ n / 2), n.MinSqFacProp ((n / 2).minSqFacAux 3)
Tactic: split_ifs with d2 d4
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
pos : ∀ (d2 : 2 ∣ n) (d4 : 2 ∣ n / 2), n.MinSqFacProp (some 2)
neg : ∀ (d2 : 2 ∣ n) (d4 : ¬2 ∣ n / 2), n.MinSqFacProp ((n / 2).minSqFacAux 3)
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)
have neg₁ : ∀ (d2 : ¬2 ∣ n), n.MinSqFacProp (n.minSqFacAux 3)
Tactic: split_ifs with d2 d4
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)
have neg : ∀ (d2 : Dvd.dvd (α := ℕ) 2 0) (d4 : ¬2 ∣ 0 / 2), MinSqFacProp 0 ((0 / 2).minSqFacAux 3)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | n0
Cleared hypotheses: n, d2, d4
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
neg : ∀ (d2 : Dvd.dvd (α := ℕ) 2 0) (d4 : ¬2 ∣ 0 / 2), MinSqFacProp 0 ((0 / 2).minSqFacAux 3)
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)
have neg₁ : ∀ (n0 : n > 0), n.MinSqFacProp ((n / 2).minSqFacAux 3)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | n0
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)
have neg : (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)
Tactic: refine minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)
have neg : ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
Tactic: refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
have neg : ∀ (p : ℕ) (pp : Prime p) (dp : p ∣ n / 2), 2 ≠ p
Tactic: refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)
have neg : ∀ (d2 : ¬Dvd.dvd (α := ℕ) 2 0), MinSqFacProp 0 (minSqFacAux 0 3)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | n0
Cleared hypotheses: n, d2
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : ¬2 ∣ n
neg : ∀ (d2 : ¬Dvd.dvd (α := ℕ) 2 0), MinSqFacProp 0 (minSqFacAux 0 3)
⊢ n.MinSqFacProp (n.minSqFacAux 3)
have neg₁ : ∀ (n0 : n > 0), n.MinSqFacProp (n.minSqFacAux 3)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | n0
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)
have neg : ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
Tactic: refine minSqFacAux_has_prop _ n0 0 rfl ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
have neg : ∀ (p : ℕ) (pp : Prime p) (dp : p ∣ n), 2 ≠ p
Tactic: refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
⊢ Prime d
have this : n.MinSqFacProp n.minSqFac
Tactic: have := minSqFac_has_prop n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ Prime d
have this₁ : n.MinSqFacProp (some d)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
⊢ d * d ∣ n
have this : n.MinSqFacProp n.minSqFac
Tactic: have := minSqFac_has_prop n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ d * d ∣ n
have this₁ : n.MinSqFacProp (some d)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ d ≤ m
have this : n.MinSqFacProp n.minSqFac
Tactic: have := minSqFac_has_prop n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m
have this₁ : n.MinSqFacProp (some d)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m
have fd : m.minFac ∣ m
Tactic: have fd := minFac_dvd m
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
⊢ Squarefree n ↔ n.minSqFac = none
have this : n.MinSqFacProp n.minSqFac
Tactic: have := minSqFac_has_prop n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n ↔ n.minSqFac = none
have mp : Squarefree n → n.minSqFac = none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
mp : Squarefree n → n.minSqFac = none
⊢ Squarefree n ↔ n.minSqFac = none
have mpr : n.minSqFac = none → Squarefree n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
⊢ n.minSqFac = none
have mp : ∀ (e : n.minSqFac = none), Eq (α := Option ℕ) none none
Tactic: rcases e : n.minSqFac with - | d
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
mp : ∀ (e : n.minSqFac = none), Eq (α := Option ℕ) none none
⊢ n.minSqFac = none
have mp₁ : ∀ (d : ℕ) (e : n.minSqFac = some d), some d = none
Tactic: rcases e : n.minSqFac with - | d
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
⊢ some d = none
have this₁ : n.MinSqFacProp (some d)
Tactic: rw [e] at this
Cleared hypotheses: this, e
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : n.minSqFac = none
⊢ Squarefree n
have mpr : ∀ (this : n.MinSqFacProp none) (H : n.minSqFac = none), Squarefree n
Tactic: rwa [H] at this
Cleared hypotheses: this, H
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
⊢ Squarefree (R := ℕ) 2
have rw : (primeFactorsList 2).Nodup
Tactic: rw [squarefree_iff_nodup_primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
rw : (primeFactorsList 2).Nodup
⊢ Squarefree (R := ℕ) 2
have rw₁ : Ne (α := ℕ) 2 0
Tactic: rw [squarefree_iff_nodup_primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
⊢ {d ∈ n.divisors | Squarefree d}.val =
    Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val
have rw : ∀ (a : ℕ),
  a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
    Membership.mem (γ := Multiset ℕ)
      (Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val) a
Tactic: rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
rw :
  ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      Membership.mem (γ := Multiset ℕ)
        (Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val) a
⊢ {d ∈ n.divisors | Squarefree d}.val =
    Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val
have rw₁ : ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
  ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
Tactic: rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
    Membership.mem (γ := Multiset ℕ)
      (Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val) a
have simp : (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a
Tactic: simp only [Multiset.mem_filter, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
      mem_divisors]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a
have mp : (a ∣ n ∧ n ≠ 0) ∧ Squarefree a → ∃ a_2 ∈ (normalizedFactors n).toFinset.powerset, a_2.val.prod = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
a : ℕ
mp : (a ∣ n ∧ n ≠ 0) ∧ Squarefree a → ∃ a_2 ∈ (normalizedFactors n).toFinset.powerset, a_2.val.prod = a
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a
have mpr : (∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a) → (a ∣ n ∧ n ≠ 0) ∧ Squarefree a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a
have h : (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a
Tactic: use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a
have h : (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Tactic: simp only [Finset.mem_powerset]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
have h : ∀ (b : ℕ) (h0 h0 : a * b ≠ 0),
  (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Tactic: rcases an with ⟨b, rfl⟩
Cleared hypotheses: n, h0_1, an, h0
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
a : ℕ
hsq : Squarefree a
b : ℕ
h0_1 h0 : a * b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
have h0₁ : a ≠ 0 ∧ b ≠ 0
Tactic: rw [mul_ne_zero_iff] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
a : ℕ
hsq : Squarefree a
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
have h : ∀ (hsq : (normalizedFactors a).Nodup) (b : ℕ) (h0 : a * b ≠ 0) (h0 : a ≠ 0 ∧ b ≠ 0),
  (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Tactic: rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
Cleared hypotheses: hsq, b, h0_1, h0
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
have h : normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a
Tactic: rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
        normalizedFactors_mul h0.1 h0.2]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ (normalizedFactors n).toFinset.powerset
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
have hs₁ : s.val ≤ (normalizedFactors n).dedup
Tactic: rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ s.val.prod ≠ 0
have rw : 0 ∉ s.val
Tactic: rw [Ne, Multiset.prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
have hs0 : s.val.prod ≠ 0
Tactic: have hs0 : s.val.prod ≠ 0 := by
        rw [Ne, Multiset.prod_eq_zero_iff]
        intro con
        apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
have mpr : (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod
Tactic: rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod
have mpr : Squarefree s.val.prod
Tactic: refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ Squarefree s.val.prod
have h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
Tactic: have h :=
        UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
          (fun x hx =>
            irreducible_of_normalized_factor x
              (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
          (prod_normalizedFactors hs0)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod
have h₁ : normalizedFactors s.val.prod = s.val
Tactic: rw [associated_eq_eq, Multiset.rel_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod
have mpr : s.val.Nodup
Tactic: rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ x = y
have rw : Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
Tactic: rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
have rw : ∀ (hx : x ⊆ (normalizedFactors n).toFinset) (y : Finset ℕ) (hy : y ⊆ (normalizedFactors n).toFinset)
  (h : x.val.prod = y.val.prod), Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
Tactic: rw [← Finset.mem_def, Finset.mem_powerset] at hx hy
Cleared hypotheses: hx, y, hy, h
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
have apply : ∀ x_1 ∈ x.val, Irreducible x_1
Tactic: apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
apply : ∀ x_1 ∈ x.val, Irreducible x_1
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
have apply₁ : ∀ x ∈ y.val, Irreducible x
Tactic: apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ Irreducible z
have apply : z ∈ normalizedFactors n
Tactic: apply irreducible_of_normalized_factor z
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ normalizedFactors n
have rw : z ∈ (normalizedFactors n).toFinset
Tactic: rw [← Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ Irreducible z
have apply : z ∈ normalizedFactors n
Tactic: apply irreducible_of_normalized_factor z
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors n
have rw : z ∈ (normalizedFactors n).toFinset
Tactic: rw [← Multiset.mem_toFinset]