awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ 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
have rw₁ : Multiset.pmap (p := PNat.Prime) (fun (p : ℕ+) (x : p.Prime) ↦ id p) v h = v
Tactic: rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ 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
have rw₂ : Multiset.map id v = v
Tactic: rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ 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
have rw₃ : v = v
Tactic: rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod
have rw : v.prod = v.prod
Tactic: rw [to_ofPNatMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ (↑(ofNatList l h).prod : ℕ) = l.prod
have this : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = (↑l : Multiset ℕ).prod
Tactic: have := prod_ofNatMultiset (l : Multiset ℕ) h
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = (↑l : Multiset ℕ).prod
⊢ (↑(ofNatList l h).prod : ℕ) = l.prod
have this₁ : (↑(ofNatMultiset (↑l : Multiset ℕ) h).prod : ℕ) = l.prod
Tactic: rw [Multiset.prod_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
⊢ (ofPNatList l h).prod = l.prod
have this : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = (↑l : Multiset ℕ+).prod
Tactic: have := prod_ofPNatMultiset (l : Multiset ℕ+) h
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = (↑l : Multiset ℕ+).prod
⊢ (ofPNatList l h).prod = l.prod
have this₁ : (ofPNatMultiset (↑l : Multiset ℕ+) h).prod = l.prod
Tactic: rw [Multiset.prod_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod
have change : Multiset.prod ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) (u + v)) = u.prod * v.prod
Tactic: change (coePNatMonoidHom (u + v)).prod = _
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u v : PrimeMultiset
⊢ Multiset.prod ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) (u + v)) = u.prod * v.prod
have rw : (HAdd.hAdd (α := Multiset ℕ+) (β := Multiset ℕ+)
      ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) u : Multiset ℕ+)
      ((coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) v : Multiset ℕ+)).prod =
  u.prod * v.prod
Tactic: rw [coePNatMonoidHom.map_add]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)
have succ : (n • u + u).prod = u.prod ^ (n + 1)
Tactic: rw [succ_nsmul, prod_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
succ : (n • u + u).prod = u.prod ^ (n + 1)
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)
have succ₁ : (n • u).prod * u.prod = u.prod ^ (n + 1)
Tactic: rw [succ_nsmul, prod_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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)
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)
have succ₂ : u.prod ^ n * u.prod = u.prod ^ (n + 1)
Tactic: rw [succ_nsmul, prod_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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)
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)
have succ₃ : u.prod ^ n * u.prod = u.prod ^ n * u.prod
Tactic: rw [succ_nsmul, prod_add, ih, pow_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
d : ℕ
u : PrimeMultiset
⊢ (d • u).prod = u.prod ^ d
have zero : (HSMul.hSMul (α := ℕ) 0 u).prod = HPow.hPow (β := ℕ) u.prod 0
Tactic: induction d with
  | zero => simp only [zero_nsmul, pow_zero, prod_zero]
  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
d : ℕ
u : PrimeMultiset
zero : (HSMul.hSMul (α := ℕ) 0 u).prod = HPow.hPow (β := ℕ) u.prod 0
⊢ (d • u).prod = u.prod ^ d
have succ : ∀ (n : ℕ) (ih : (n • u).prod = u.prod ^ n), ((n + 1) • u).prod = u.prod ^ (n + 1)
Tactic: induction d with
  | zero => simp only [zero_nsmul, pow_zero, prod_zero]
  | succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n : ℕ+
⊢ (↑(PrimeMultiset.ofNatList (↑n : ℕ).primeFactorsList ⋯).prod : ℕ) = (↑n : ℕ)
have rw : (↑n : ℕ).primeFactorsList.prod = (↑n : ℕ)
Tactic: rw [PrimeMultiset.prod_ofNatList]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
⊢ v.prod.factorMultiset = v
have a : v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
Tactic: apply PrimeMultiset.coeNat_injective
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
have a : (↑v.toNatMultiset.prod.primeFactorsList : Multiset ℕ) = v.toNatMultiset
Tactic: rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
⊢ (↑v.toNatMultiset.prod.primeFactorsList : Multiset ℕ) = v.toNatMultiset
have 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)
Tactic: rcases v with ⟨l⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
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
have hp₁ : ∃ (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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) l
⊢ (↑(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 ℕ)
have this : ∀ (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'
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset
have this : n = u.prod
Tactic: have : n = u.prod := (prod_factorMultiset n).symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset
have rw : (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
have this₁ : m = v.prod
Tactic: have : m = v.prod := (prod_factorMultiset m).symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
have rw : (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
have rw : (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
Tactic: rw [← PrimeMultiset.prod_add]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
have rw : u + v = u.prod.factorMultiset + v.prod.factorMultiset
Tactic: rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset
have rw : u + v = u + v.prod.factorMultiset
Tactic: rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset
have rw : u + v = u + v
Tactic: rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this_1 : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
have repeat' : u + v = u.prod.factorMultiset + v.prod.factorMultiset
Tactic: repeat' rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
have repeat'₃ : u + v = u + v.prod.factorMultiset
Tactic: repeat' rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
⊢ (n ^ m).factorMultiset = m • n.factorMultiset
have this : n = u.prod
Tactic: have : n = u.prod := (prod_factorMultiset n).symm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset
have rw : (m • u).prod.factorMultiset = m • u.prod.factorMultiset
Tactic: rw [this, ← PrimeMultiset.prod_smul]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset
have rw : m • u = m • u.prod.factorMultiset
Tactic: rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset
have rw : m • u = m • u
Tactic: rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset
have repeat' : m • u = m • u.prod.factorMultiset
Tactic: repeat' rw [PrimeMultiset.factorMultiset_prod]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
p : Nat.Primes
⊢ (↑p : ℕ+).factorMultiset = PrimeMultiset.ofPrime p
have a : Eq (α := ℕ+) ((factorMultisetEquiv.symm : (a : PrimeMultiset) → ℕ+) (↑p : ℕ+).factorMultiset : ℕ+)
  ((factorMultisetEquiv.symm : (a : PrimeMultiset) → ℕ+) (PrimeMultiset.ofPrime p) : ℕ+)
Tactic: apply factorMultisetEquiv.symm.injective
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
p : Nat.Primes
⊢ (↑p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
have a : (↑p : ℕ+) = (PrimeMultiset.ofPrime p).prod
Tactic: rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
p : Nat.Primes
a : (↑p : ℕ+) = (PrimeMultiset.ofPrime p).prod
⊢ (↑p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
have a₁ : (↑p : ℕ+) = (↑p : ℕ+)
Tactic: rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n
have mp : m.factorMultiset ≤ n.factorMultiset → m ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
mp : m.factorMultiset ≤ n.factorMultiset → m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n
have mpr : m ∣ n → m.factorMultiset ≤ n.factorMultiset
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m ∣ n
have mp : m.factorMultiset.prod.factorMultiset.prod ∣ n
Tactic: rw [← prod_factorMultiset m, ← prod_factorMultiset m]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod ∣ n
have mp : m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
Tactic: apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
have mp : (m.factorMultiset.prod.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
Tactic: rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
mp : (m.factorMultiset.prod.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
have mp₁ : (m.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
Tactic: rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
have mp₂ : n.factorMultiset.prod = n
Tactic: rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
have mp₃ : n = n
Tactic: rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset
have mpr : m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset
Tactic: rw [← mul_div_exact h, factorMultiset_mul]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
u v : PrimeMultiset
h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := ⋯
⊢ u.prod ∣ v.prod ↔ u ≤ v
have h₁ : u ≤ v ↔ u.prod ∣ v.prod
Tactic: rw [u.factorMultiset_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset
have a : (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset
have a₁ : m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset
have a : (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset
Tactic: apply le_inf_iff.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset
have a : (m.gcd n).factorMultiset ≤ m.factorMultiset
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : (m.gcd n).factorMultiset ≤ m.factorMultiset
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset
have a₁ : (m.gcd n).factorMultiset ≤ n.factorMultiset
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset
have a : m.gcd n ∣ m
Tactic: apply factorMultiset_le_iff.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ n.factorMultiset
have a : m.gcd n ∣ n
Tactic: apply factorMultiset_le_iff.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
have a : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n
Tactic: rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n
have a : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m
Tactic: apply dvd_gcd
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n
have a₁ : (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n
Tactic: apply dvd_gcd
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m
have a : m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset
Tactic: rw [PrimeMultiset.prod_dvd_iff']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ n
have a : m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset
Tactic: rw [PrimeMultiset.prod_dvd_iff']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset
have a : (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset
have a₁ : m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
have a : m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Tactic: rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
have a : m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
have a₁ : n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
have a : m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Tactic: rw [← factorMultiset_le_iff']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
have a : n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Tactic: rw [← factorMultiset_le_iff']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset
have a : m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset
Tactic: apply sup_le_iff.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset
have a : m.factorMultiset ≤ (m.lcm n).factorMultiset
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
a : m.factorMultiset ≤ (m.lcm n).factorMultiset
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset
have a₁ : n.factorMultiset ≤ (m.lcm n).factorMultiset
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset
have a : m ∣ m.lcm n
Tactic: apply factorMultiset_le_iff.mpr
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
m n : ℕ+
⊢ n.factorMultiset ≤ (m.lcm n).factorMultiset
have a : n ∣ m.lcm n
Tactic: apply factorMultiset_le_iff.mpr