awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact IH n (dvd_refl _) dk

Premises used: dvd_refl
-- Module: Mathlib.Data.Nat.Squarefree
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)
neg₁ : ∀ (d2 : ¬2 ∣ n), n.MinSqFacProp (n.minSqFacAux 3)
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)

Tactic:
split_ifs with d2 d4
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

Tactic:
⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩

Premises used: Nat.prime_two, Nat.MinSqFacProp, And.intro, Iff.mp, Nat.Prime.two_le, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

Tactic:
exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩
-- Module: Mathlib.Data.Nat.Squarefree
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)
neg₁ : ∀ (n0 : n > 0), n.MinSqFacProp ((n / 2).minSqFacAux 3)
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | n0

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
d2 : Dvd.dvd (α := ℕ) 2 0
d4 : ¬2 ∣ 0 / 2
⊢ 2 ∣ 0 / 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
d2 : Dvd.dvd (α := ℕ) 2 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 ((0 / 2).minSqFacAux 3)

Tactic:
cases d4 (by decide)
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_

Premises used: Iff.mpr, mt, Nat.prime_two, Nat.minSqFacProp_div, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
neg : (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
refine minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_

Premises used: Iff.mpr, mt, Nat.prime_two, Nat.minSqFacProp_div, Nat.dvd_div_iff_mul_dvd
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
neg : ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
⊢ (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_

Premises used: Nat.minSqFacAux_has_prop, OfNat.ofNat, Nat.le_of_dvd, Nat.div_pos, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m

Tactic:
fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Premises used: Nat.succ_le_of_lt, Nat.Prime.two_le, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
neg : ∀ (p : ℕ) (pp : Prime p) (dp : p ∣ n / 2), 2 ≠ p
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Premises used: Nat.succ_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
neg : ∀ (d2 : ¬Dvd.dvd (α := ℕ) 2 0), MinSqFacProp 0 (minSqFacAux 0 3)
neg₁ : ∀ (n0 : n > 0), n.MinSqFacProp (n.minSqFacAux 3)
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | n0

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
d2 : ¬Dvd.dvd (α := ℕ) 2 0
⊢ Dvd.dvd (α := ℕ) 2 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
d2 : ¬Dvd.dvd (α := ℕ) 2 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)

Tactic:
cases d2 (by decide)
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
minSqFacAux_has_prop _ n0 0 rfl ?_

Premises used: Nat.minSqFacAux_has_prop, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
neg : ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
refine minSqFacAux_has_prop _ n0 0 rfl ?_

Premises used: Nat.minSqFacAux_has_prop, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m

Tactic:
fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Premises used: Nat.succ_le_of_lt, Nat.Prime.two_le, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
neg : ∀ (p : ℕ) (pp : Prime p) (dp : p ∣ n), 2 ≠ p
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Premises used: Nat.succ_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
⊢ n.MinSqFacProp n.minSqFac

Tactic:
have := minSqFac_has_prop n
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ n.MinSqFacProp (some d)

Tactic:
rw [h] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n

Tactic:
this.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n

Tactic:
exact this.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ n.MinSqFacProp n.minSqFac

Tactic:
have := minSqFac_has_prop n
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ n.MinSqFacProp (some d)

Tactic:
rw [h] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ m.minFac ∣ m

Tactic:
have fd := minFac_dvd m
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ d ≤ m

Tactic:
exact
    le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
      (minFac_le <| lt_of_lt_of_le (by decide) m2)

Premises used: Nat.minFac_le, mul_dvd_mul, dvd_trans, And.right, Nat.minFac_prime, lt_of_lt_of_le, Nat.ne_of_gt, le_trans
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
⊢ n.MinSqFacProp n.minSqFac

Tactic:
have := minSqFac_has_prop n
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
mp : Squarefree n → n.minSqFac = none
mpr : n.minSqFac = none → Squarefree n
⊢ Squarefree n ↔ n.minSqFac = none

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
mp : ∀ (e : n.minSqFac = none), Eq (α := Option ℕ) none none
mp₁ : ∀ (d : ℕ) (e : n.minSqFac = some d), some d = none
⊢ n.minSqFac = none

Tactic:
rcases e : n.minSqFac with - | d

Premises used: Nat.minSqFac
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
e : n.minSqFac = none
⊢ Eq (α := Option ℕ) none none

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
⊢ n.MinSqFacProp (some d)

Tactic:
rw [e] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : Squarefree n
d : ℕ
e : n.minSqFac = some d
this₁ : n.MinSqFacProp (some d)
⊢ n.minSqFac = some d

Tactic:
rw [e] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none

Tactic:
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1

Premises used: And.right, And.left, Iff.mp, Nat.squarefree_iff_prime_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : n.minSqFac = none
mpr mpr₁ mpr₂ mpr₃ : ∀ (this : n.MinSqFacProp none) (H : n.minSqFac = none), Squarefree n
⊢ Squarefree n

Tactic:
rwa [H] at this
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
rw : (primeFactorsList 2).Nodup
rw₁ : Ne (α := ℕ) 2 0
⊢ Squarefree (R := ℕ) 2

Tactic:
rw [squarefree_iff_nodup_primeFactorsList]

Premises used: Nat.squarefree_iff_nodup_primeFactorsList
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
⊢ (primeFactorsList 2).Nodup

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
⊢ {d ∈ n.divisors | Squarefree d} = n.divisors

Tactic:
Finset.ext fun d => ⟨@Finset.filter_subset _ _ _ _ d, fun hd =>
    Finset.mem_filter.mpr ⟨hd, hn.squarefree_of_dvd (Nat.dvd_of_mem_divisors hd) ⟩⟩

Premises used: Iff.mpr, Finset.ext, Finset.filter_subset, Nat.dvd_of_mem_divisors, Squarefree.squarefree_of_dvd, Nat.divisors, And.intro, Iff.intro, Finset.mem_filter, Squarefree
-- Module: Mathlib.Data.Nat.Squarefree
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
rw₁ :
  ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
⊢ {d ∈ n.divisors | Squarefree d}.val =
    Multiset.map (fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]

Premises used: Finset.nodup, Multiset.Nodup.ext, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
a : ℕ
simp : (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = 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:
simp only [Multiset.mem_filter, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
      mem_divisors]

Premises used: Nat.mem_divisors, Multiset.mem_map, Finset.filter_val, Multiset.mem_filter, Finset.mem_def
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
a : ℕ
mp : (a ∣ n ∧ n ≠ 0) ∧ Squarefree a → ∃ a_2 ∈ (normalizedFactors n).toFinset.powerset, a_2.val.prod = a
mpr : (∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a) → (a ∣ n ∧ n ≠ 0) ∧ Squarefree a
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
h :
  (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a
⊢ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a

Tactic:
use (UniqueFactorizationMonoid.normalizedFactors a).toFinset

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.toFinset
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
h : (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
⊢ (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
simp only [Finset.mem_powerset]

Premises used: Finset.mem_powerset
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0_1 : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
h :
  ∀ (b : ℕ) (h0 h0 : a * b ≠ 0),
    (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rcases an with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
a : ℕ
hsq : Squarefree a
b : ℕ
h0_1 h0 : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [mul_ne_zero_iff] at h0

Premises used: mul_ne_zero_iff
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
a : ℕ
hsq : Squarefree a
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
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
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq

Premises used: And.left, UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
h : normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
        normalizedFactors_mul h0.1 h0.2]

Premises used: UniqueFactorizationMonoid.normalizedFactors_mul, associated_iff_eq, And.right, And.left, Multiset.toFinset_subset, Multiset.Nodup.dedup, Multiset.toFinset_val
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a

Tactic:
⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩

Premises used: Multiset.subset_of_le, And.left, UniqueFactorizationMonoid.prod_normalizedFactors, And.intro, Multiset.le_add_right
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0_1 : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a

Tactic:
exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ (normalizedFactors n).toFinset.powerset
⊢ s.val ≤ (normalizedFactors n).dedup

Tactic:
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs

Premises used: Finset.mem_powerset, Finset.val_le_iff, Multiset.toFinset_val
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
rw : 0 ∉ s.val
⊢ s.val.prod ≠ 0

Tactic:
rw [Ne, Multiset.prod_eq_zero_iff]

Premises used: Multiset.prod_eq_zero_iff, Ne
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
con : 0 ∈ s.val
⊢ False

Tactic:
apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))

Premises used: Multiset.mem_dedup, Multiset.mem_of_le, not_irreducible_zero, Iff.mp, UniqueFactorizationMonoid.irreducible_of_normalized_factor, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ 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)))
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
mpr : (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]

Premises used: Associated.symm, UniqueFactorizationMonoid.prod_normalizedFactors, Associated.dvd_iff_dvd_right
-- Module: Mathlib.Data.Nat.Squarefree
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

Tactic:
⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩

Premises used: Multiset.prod_dvd_prod_of_le, Multiset.dedup_le, And.intro, le_trans
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
mpr : Squarefree s.val.prod
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ 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)
-- Module: Mathlib.Data.Nat.Squarefree
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
⊢ normalizedFactors s.val.prod = s.val

Tactic:
rw [associated_eq_eq, Multiset.rel_eq] at h

Premises used: associated_eq_eq, Multiset.rel_eq
-- Module: Mathlib.Data.Nat.Squarefree
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
mpr : s.val.Nodup
⊢ Squarefree s.val.prod

Tactic:
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]

Premises used: UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
-- Module: Mathlib.Data.Nat.Squarefree
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
⊢ s.val.Nodup

Tactic:
apply s.nodup

Premises used: Finset.nodup
-- Module: Mathlib.Data.Nat.Squarefree
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
rw : Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val
⊢ x = y

Tactic:
rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]

Premises used: associated_eq_eq, Multiset.rel_eq, Finset.val_inj
-- Module: Mathlib.Data.Nat.Squarefree
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
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
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val

Tactic:
rw [← Finset.mem_def, Finset.mem_powerset] at hx hy

Premises used: Finset.mem_powerset, Finset.mem_def
-- Module: Mathlib.Data.Nat.Squarefree
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
apply₁ : ∀ x ∈ y.val, Irreducible x
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) x.val y.val

Tactic:
apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)

Premises used: Iff.mpr, UniqueFactorizationMonoid.factors_unique, associated_iff_eq
-- Module: Mathlib.Data.Nat.Squarefree
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
apply : z ∈ normalizedFactors n
apply₁ : ℕ
⊢ Irreducible z

Tactic:
apply irreducible_of_normalized_factor z

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.Data.Nat.Squarefree
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
rw : z ∈ (normalizedFactors n).toFinset
⊢ z ∈ normalizedFactors n

Tactic:
rw [← Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.Nat.Squarefree
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).toFinset

Tactic:
apply hx hz
-- Module: Mathlib.Data.Nat.Squarefree
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
apply : z ∈ normalizedFactors n
apply₁ : ℕ
⊢ Irreducible z

Tactic:
apply irreducible_of_normalized_factor z

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.Data.Nat.Squarefree
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
rw : z ∈ (normalizedFactors n).toFinset
⊢ z ∈ normalizedFactors n

Tactic:
rw [← Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Data.Nat.Squarefree
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).toFinset

Tactic:
apply hy hz
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst : AddCommMonoid α
f : ℕ → α
rw :
  (Multiset.map (f ∘ fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    Multiset.sum (Multiset.map (fun (i : Finset ℕ) ↦ f i.val.prod) (normalizedFactors n).toFinset.powerset.val)
⊢ Eq.{u_1 + 1} (α := α) (∑ d ∈ n.divisors with Squarefree d, f d)
    (∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod)

Tactic:
rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map,
    Finset.sum_eq_multiset_sum]

Premises used: Finset.sum_eq_multiset_sum, Multiset.map_map, Nat.divisors_filter_squarefree
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun (x : Finset ℕ) ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    Multiset.sum (Multiset.map (fun (i : Finset ℕ) ↦ f i.val.prod) (normalizedFactors n).toFinset.powerset.val)

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

Tactic:
use 1