awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ Eq (α := (p : ℕ+) → (h : p.Prime) → ℕ+)
    (fun (p : ℕ+) (h : p.Prime) ↦ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+))
    fun (p : ℕ+) (x : p.Prime) ↦ id p

Tactic:
have : (fun (p : ℕ+) (h : p.Prime) => ((↑) : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p := by
    funext p h
    apply Subtype.ext
    rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this :
  Eq (α := (p : ℕ+) → (h : p.Prime) → ℕ+)
    (fun (p : ℕ+) (h : p.Prime) ↦ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+))
    fun (p : ℕ+) (x : p.Prime) ↦ id p
rw :
  Multiset.pmap (p := PNat.Prime)
      (fun (a : ℕ+) (h : a.Prime) ↦ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑a : ℕ) h) : ℕ+)) v h =
    v
rw₁ : Multiset.pmap (p := PNat.Prime) (fun (p : ℕ+) (x : p.Prime) ↦ id p) v h = v
rw₂ : Multiset.map id v = v
rw₃ rw₄ : v = v
⊢ Multiset.map Nat.Primes.toPNat
      (Multiset.pmap (p := PNat.Prime)
        (fun (p : ℕ+) (hp : p.Prime) ↦ Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) hp) v h) =
    v

Tactic:
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]

Premises used: Multiset.map_id, Multiset.pmap_eq_map, Multiset.map_pmap
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
rw rw₁ : v.prod = v.prod
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod

Tactic:
rw [to_ofPNatMultiset]

Premises used: PrimeMultiset.to_ofPNatMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : ℕ+
l : List ℕ
hl : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ p ∈ (ofNatList l hl).toPNatMultiset ↔ (↑p : ℕ) ∈ l

Tactic:
simp [ofNatList]

Premises used: PrimeMultiset.ofNatList
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = (↑l : Multiset ℕ).prod

Tactic:
have := prod_ofNatMultiset (l : Multiset ℕ) h
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = (↑l : Multiset ℕ).prod
⊢ (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Premises used: Multiset.prod_coe
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = l.prod
⊢ (↑(ofNatList l h).prod : ℕ) = l.prod

Tactic:
this

Premises used: PrimeMultiset.ofNatList
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = l.prod
⊢ (↑(ofNatList l h).prod : ℕ) = l.prod

Tactic:
exact this
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ+
hl : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatList l hl).toPNatMultiset = (↑l : Multiset ℕ+)

Tactic:
simp [ofPNatList]

Premises used: PrimeMultiset.ofPNatList
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = (↑l : Multiset ℕ+).prod

Tactic:
have := prod_ofPNatMultiset (l : Multiset ℕ+) h
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = (↑l : Multiset ℕ+).prod
⊢ (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Premises used: Multiset.prod_coe
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
this

Premises used: PrimeMultiset.ofPNatList
-- Module: Mathlib.Data.PNat.Factors
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
exact this
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ prod 0 = 1

Tactic:
Multiset.prod_zero

Premises used: Multiset.prod_zero, Multiset.map, List.map, PrimeMultiset.toPNatMultiset, PrimeMultiset.prod, Multiset.zero, Multiset.ofList
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ prod 0 = 1

Tactic:
exact Multiset.prod_zero

Premises used: Multiset.prod_zero
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
change : Multiset.prod ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) (u + v)) = u.prod * v.prod
⊢ (u + v).prod = u.prod * v.prod

Tactic:
change (coePNatMonoidHom (u + v)).prod = _

Premises used: Multiset.prod, PrimeMultiset.coePNatMonoidHom, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
rw :
  (HAdd.hAdd (α := Multiset ℕ+) (β := Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) u : Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) v : Multiset ℕ+)).prod =
    u.prod * v.prod
⊢ Multiset.prod ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) (u + v)) = u.prod * v.prod

Tactic:
rw [coePNatMonoidHom.map_add]

Premises used: PrimeMultiset.coePNatMonoidHom, AddMonoidHom.map_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
⊢ (HAdd.hAdd (α := Multiset ℕ+) (β := Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) u : Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) v : Multiset ℕ+)).prod =
    u.prod * v.prod

Tactic:
Multiset.prod_add _ _

Premises used: Multiset.map, PrimeMultiset.toPNatMultiset, PrimeMultiset.prod, Multiset.prod_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
⊢ (HAdd.hAdd (α := Multiset ℕ+) (β := Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) u : Multiset ℕ+)
        ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) v : Multiset ℕ+)).prod =
    u.prod * v.prod

Tactic:
exact Multiset.prod_add _ _

Premises used: Multiset.prod_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
u : PrimeMultiset
⊢ (HSMul.hSMul (α := ℕ) 0 u).prod = HPow.hPow (β := ℕ) u.prod 0

Tactic:
simp only [zero_nsmul, pow_zero, prod_zero]

Premises used: pow_zero, zero_nsmul, PrimeMultiset.prod_zero
-- Module: Mathlib.Data.PNat.Factors
Goal:
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
succ : (n • u + u).prod = u.prod ^ (n + 1)
succ₁ : (n • u).prod * u.prod = u.prod ^ (n + 1)
succ₂ : u.prod ^ n * u.prod = u.prod ^ (n + 1)
succ₃ succ₄ : u.prod ^ n * u.prod = u.prod ^ n * u.prod
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)

Tactic:
rw [succ_nsmul, prod_add, ih, pow_succ]

Premises used: pow_succ, PrimeMultiset.prod_add, succ_nsmul
-- Module: Mathlib.Data.PNat.Factors
Goal:
d : ℕ
u : PrimeMultiset
zero : (HSMul.hSMul (α := ℕ) 0 u).prod = HPow.hPow (β := ℕ) u.prod 0
succ : ∀ (n : ℕ) (ih : (n • u).prod = u.prod ^ n), ((n + 1) • u).prod = u.prod ^ (n + 1)
⊢ (d • u).prod = u.prod ^ d

Tactic:
induction d with
  | zero => simp only [zero_nsmul, pow_zero, prod_zero]
  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]

Premises used: pow_succ, PrimeMultiset.prod_add, pow_zero, zero_nsmul, PrimeMultiset.prod_zero, succ_nsmul
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
rw : (↑n : ℕ).primeFactorsList.prod = (↑n : ℕ)
⊢ (↑(PrimeMultiset.ofNatList (↑n : ℕ).primeFactorsList ⋯).prod : ℕ) = (↑n : ℕ)

Tactic:
rw [PrimeMultiset.prod_ofNatList]

Premises used: PrimeMultiset.prod_ofNatList
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
⊢ (↑n : ℕ).primeFactorsList.prod = (↑n : ℕ)

Tactic:
Nat.prod_primeFactorsList n.ne_zero

Premises used: PNat.ne_zero, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
⊢ (↑n : ℕ).primeFactorsList.prod = (↑n : ℕ)

Tactic:
exact Nat.prod_primeFactorsList n.ne_zero

Premises used: PNat.ne_zero, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
⊢ n.factorMultiset.toNatMultiset = (↑(↑n : ℕ).primeFactorsList : Multiset ℕ)

Tactic:
PrimeMultiset.to_ofNatMultiset (Nat.primeFactorsList n) (@Nat.prime_of_mem_primeFactorsList n)

Premises used: PNat.val, Nat.prime_of_mem_primeFactorsList, PrimeMultiset.ofNatList, Multiset.ofList, PNat.factorMultiset, PrimeMultiset.to_ofNatMultiset, Nat.primeFactorsList
-- Module: Mathlib.Data.PNat.Factors
Goal:
p n : ℕ+
⊢ p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n

Tactic:
simp [factorMultiset, dvd_iff, PNat.Prime]

Premises used: PNat.dvd_iff, PNat.factorMultiset, PNat.Prime
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
a : v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
⊢ v.prod.factorMultiset = v

Tactic:
apply PrimeMultiset.coeNat_injective

Premises used: PrimeMultiset.coeNat_injective
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
a : (↑v.toNatMultiset.prod.primeFactorsList : Multiset ℕ) = v.toNatMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset

Tactic:
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]

Premises used: PrimeMultiset.prod, PNat.coeNat_factorMultiset, PrimeMultiset.coe_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
a :
  ∀ (l : List Nat.Primes),
    (↑(toNatMultiset
                (Quot.mk (⇑(List.isSetoid Nat.Primes) : List Nat.Primes → List Nat.Primes → Prop)
                  l)).prod.primeFactorsList :
        Multiset ℕ) =
      toNatMultiset (Quot.mk (⇑(List.isSetoid Nat.Primes) : List Nat.Primes → List Nat.Primes → Prop) l)
⊢ (↑v.toNatMultiset.prod.primeFactorsList : Multiset ℕ) = v.toNatMultiset

Tactic:
rcases v with ⟨l⟩
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
p : ℕ
hp : p ∈ l'
⊢ ∃ (h : Nat.Prime p), Subtype.mk (p := fun (x : ℕ) ↦ Nat.Prime x) p h ∈ l

Tactic:
simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp

Premises used: List.map_subtype, List.map_id_fun', List.mem_unattach, id_eq
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
p : ℕ
hp : ∃ (h : Nat.Prime p), Subtype.mk (p := fun (x : ℕ) ↦ Nat.Prime x) p h ∈ l
⊢ Nat.Prime p

Tactic:
obtain ⟨hp', -⟩ := hp
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
p : ℕ
hp' : Nat.Prime p
⊢ Nat.Prime p

Tactic:
hp'
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
p : ℕ
hp' : Nat.Prime p
⊢ Nat.Prime p

Tactic:
exact hp'
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
⊢ ∀ (p : ℕ) (hp : p ∈ l'), Nat.Prime p

Tactic:
have (p : ℕ) (hp : p ∈ l') : p.Prime := by
    simp only [List.map_subtype, List.map_id_fun', id_eq, List.mem_unattach, l'] at hp
    obtain ⟨hp', -⟩ := hp
    exact hp'
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
this : ∀ (p : ℕ) (hp : p ∈ l'), Nat.Prime p
⊢ (↑(List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l).prod.primeFactorsList : Multiset ℕ) =
    (↑(List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l) : Multiset ℕ)

Tactic:
Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm

Premises used: Iff.mpr, Multiset.coe_eq_coe, Nat.primeFactorsList_unique, List.Perm.symm, rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
this : ∀ (p : ℕ) (hp : p ∈ l'), Nat.Prime p
⊢ (↑(List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l).prod.primeFactorsList : Multiset ℕ) =
    (↑(List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l) : Multiset ℕ)

Tactic:
exact Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm

Premises used: Iff.mpr, Multiset.coe_eq_coe, Nat.primeFactorsList_unique, List.Perm.symm, rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ factorMultiset 1 = 0

Tactic:
simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]

Premises used: PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset, PNat.factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
⊢ n = u.prod

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
rw : (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ m = v.prod

Tactic:
have : m = v.prod := (prod_factorMultiset m).symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
rw : (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset

Tactic:
rw [this]
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
rw : (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
⊢ (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_add]

Premises used: PrimeMultiset.prod_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
rw : u + v = u.prod.factorMultiset + v.prod.factorMultiset
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
rw : u + v = u + v.prod.factorMultiset
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
rw rw₁ : u + v = u + v
⊢ u + v = u + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
repeat' repeat'₁ repeat'₂ : u + v = u.prod.factorMultiset + v.prod.factorMultiset
repeat'₃ : u + v = u + v.prod.factorMultiset
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
⊢ n = u.prod

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
rw : (m • u).prod.factorMultiset = m • u.prod.factorMultiset
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
rw [this, ← PrimeMultiset.prod_smul]

Premises used: PrimeMultiset.prod_smul
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
rw : m • u = m • u.prod.factorMultiset
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
rw rw₁ : m • u = m • u
⊢ m • u = m • u.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
repeat' repeat'₁ repeat'₂ : m • u = m • u.prod.factorMultiset
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
a :
  Eq (α := ℕ+) ((factorMultisetEquiv.symm : (a : PrimeMultiset) → ℕ+) (↑p : ℕ+).factorMultiset : ℕ+)
    ((factorMultisetEquiv.symm : (a : PrimeMultiset) → ℕ+) (PrimeMultiset.ofPrime p) : ℕ+)
⊢ (↑p : ℕ+).factorMultiset = PrimeMultiset.ofPrime p

Tactic:
apply factorMultisetEquiv.symm.injective

Premises used: PNat.factorMultisetEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
a : (↑p : ℕ+) = (PrimeMultiset.ofPrime p).prod
a₁ a₂ : (↑p : ℕ+) = (↑p : ℕ+)
⊢ (↑p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Tactic:
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]

Premises used: Nat.Primes.toPNat, PrimeMultiset.prod_ofPrime, PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
mp : m.factorMultiset ≤ n.factorMultiset → m ∣ n
mpr : m ∣ n → m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
mp : m.factorMultiset.prod.factorMultiset.prod ∣ n
⊢ m ∣ n

Tactic:
rw [← prod_factorMultiset m, ← prod_factorMultiset m]

Premises used: PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
mp : m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
⊢ m.factorMultiset.prod.factorMultiset.prod ∣ n

Tactic:
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod

Premises used: Dvd.intro, HSub.hSub, PrimeMultiset.prod, PNat.factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
mp : (m.factorMultiset.prod.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
mp₁ : (m.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
mp₂ : n.factorMultiset.prod = n
mp₃ mp₄ : n = n
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n

Tactic:
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]

Premises used: PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, PNat.prod_factorMultiset, add_tsub_cancel_of_le
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m ∣ n
mpr : m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset
⊢ m.factorMultiset ≤ n.factorMultiset

Tactic:
rw [← mul_div_exact h, factorMultiset_mul]

Premises used: PNat.factorMultiset_mul, PNat.mul_div_exact
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v.prod.factorMultiset ↔ m ∣ v.prod := ⋯
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
rw [v.factorMultiset_prod] at h

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
h
-- Module: Mathlib.Data.PNat.Factors
Goal:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
exact h
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := ⋯
⊢ u ≤ v ↔ u.prod ∣ v.prod

Tactic:
rw [u.factorMultiset_prod] at h

Premises used: PrimeMultiset.factorMultiset_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
h.symm

Premises used: Iff.symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
exact h.symm

Premises used: Iff.symm
-- Module: Mathlib.Data.PNat.Factors
Goal:
u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n.factorMultiset.prod ↔ u ≤ n.factorMultiset := ⋯
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
rw [n.prod_factorMultiset] at h

Premises used: PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n ↔ u ≤ n.factorMultiset
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
h
-- Module: Mathlib.Data.PNat.Factors
Goal:
u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n ↔ u ≤ n.factorMultiset
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
exact h
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset
a₁ : m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset

Tactic:
apply le_inf_iff.mpr

Premises used: Iff.mpr, le_inf_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.gcd n).factorMultiset ≤ m.factorMultiset
a₁ : (m.gcd n).factorMultiset ≤ n.factorMultiset
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.gcd n ∣ m
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset

Tactic:
apply factorMultiset_le_iff.mpr

Premises used: Iff.mpr, PNat.factorMultiset_le_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.gcd n ∣ n
⊢ (m.gcd n).factorMultiset ≤ n.factorMultiset

Tactic:
apply factorMultiset_le_iff.mpr

Premises used: Iff.mpr, PNat.factorMultiset_le_iff
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.gcd n ∣ m

Tactic:
gcd_dvd_left m n

Premises used: PNat.gcd_dvd_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.gcd n ∣ m

Tactic:
exact gcd_dvd_left m n

Premises used: PNat.gcd_dvd_left
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.gcd n ∣ n

Tactic:
gcd_dvd_right m n

Premises used: PNat.gcd_dvd_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.gcd n ∣ n

Tactic:
exact gcd_dvd_right m n

Premises used: PNat.gcd_dvd_right
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Premises used: PrimeMultiset.prod_dvd_iff, PNat.prod_factorMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m
a₁ : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n

Tactic:
apply dvd_gcd

Premises used: PNat.dvd_gcd
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m

Tactic:
rw [PrimeMultiset.prod_dvd_iff']

Premises used: PrimeMultiset.prod_dvd_iff'
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
a : m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n

Tactic:
rw [PrimeMultiset.prod_dvd_iff']

Premises used: PrimeMultiset.prod_dvd_iff'
-- Module: Mathlib.Data.PNat.Factors
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

Tactic:
inf_le_left

Premises used: inf_le_left