awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
rw :
  (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑m : ℕ) ∧
    (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑k : ℕ)
⊢ (↑(m.mod k) : ℕ) ≤ (↑m : ℕ) ∧ (↑(m.mod k) : ℕ) ≤ (↑k : ℕ)

Tactic:
rw [mod_coe]

Premises used: PNat.mod_coe
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
pos : ∀ (h : (↑m : ℕ) % (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
neg : ∀ (h : ¬(↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑m : ℕ) % (↑k : ℕ) ≤ (↑k : ℕ)
⊢ (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑m : ℕ) ∧
    (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑k : ℕ)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) > 0

Tactic:
have hm : (m : ℕ) > 0 := m.pos
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑m : ℕ) > 0
pos : ∀ (hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
⊢ (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢

Premises used: PNat.val, zero_add, Nat.mod_add_div
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
pos : ∀ (h₁ : (↑m : ℕ) / (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
neg : ∀ (h₁ : ¬(↑m : ℕ) / (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
by_cases h₁ : (m : ℕ) / (k : ℕ) = 0

Premises used: PNat.val
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ GT.gt (α := ℕ) 0 0

Tactic:
rw [h₁, mul_zero] at hm

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : (↑m : ℕ) / (↑k : ℕ) = 0
hm₁ : GT.gt (α := ℕ) 0 0
⊢ (↑m : ℕ) / (↑k : ℕ) = 0

Tactic:
rw [h₁, mul_zero] at hm

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : GT.gt (α := ℕ) 0 0
h₁ : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
(lt_irrefl _ hm).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : GT.gt (α := ℕ) 0 0
h₁ : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
exact (lt_irrefl _ hm).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : ¬(↑m : ℕ) / (↑k : ℕ) = 0
h₂ : (↑k : ℕ) * 1 ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) := ⋯
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))

Tactic:
rw [mul_one] at h₂

Premises used: mul_one
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : ¬(↑m : ℕ) / (↑k : ℕ) = 0
h₂ : (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
⟨h₂, le_refl (k : ℕ)⟩

Premises used: PNat.val, le_refl, And.intro
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : ¬(↑m : ℕ) / (↑k : ℕ) = 0
h₂ : (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
exact ⟨h₂, le_refl (k : ℕ)⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : ¬(↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑m : ℕ) % (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩

Premises used: PNat.val, LT.lt.le, Nat.mod_lt, PNat.pos, And.intro, Nat.mod_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : ¬(↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑m : ℕ) % (↑k : ℕ) ≤ (↑k : ℕ)

Tactic:
exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
mp : k ∣ m → (↑k : ℕ) ∣ (↑m : ℕ)
mpr : (↑k : ℕ) ∣ (↑m : ℕ) → k ∣ m
⊢ k ∣ m ↔ (↑k : ℕ) ∣ (↑m : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : k ∣ m
mp : ∀ (w : ℕ+), (↑k : ℕ) ∣ (↑(k * w) : ℕ)
⊢ (↑k : ℕ) ∣ (↑m : ℕ)

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
k w : ℕ+
⊢ (↑k : ℕ) ∣ (↑(k * w) : ℕ)

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : (↑k : ℕ) ∣ (↑m : ℕ)
mpr : ∀ (a : ℕ) (h : (↑m : ℕ) = (↑k : ℕ) * a), k ∣ m
⊢ k ∣ m

Tactic:
rcases h with ⟨a, h⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : (↑m : ℕ) = (↑k : ℕ) * 0
⊢ False

Tactic:
simp only [mul_zero, ne_zero] at h

Premises used: PNat.ne_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
a : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * a
mpr : ∀ (n : ℕ) (h : (↑m : ℕ) = (↑k : ℕ) * n.succ), k ∣ m
⊢ k ∣ m

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
      rintro rfl
      simp only [mul_zero, ne_zero] at h

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
n : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * n.succ
h₁ : m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯
⊢ k ∣ m

Tactic:
use ⟨n.succ, n.succ_pos⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
n : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * n.succ
h₁ : (↑m : ℕ) = (↑(k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯) : ℕ)
h₂ : (↑k : ℕ) * n.succ = (↑(k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯) : ℕ)
h₃ : (↑k : ℕ) * n.succ = (↑k : ℕ) * (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯) : ℕ)
h₄ h₅ : (↑k : ℕ) * n.succ = (↑k : ℕ) * n.succ
⊢ m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯

Tactic:
rw [← coe_inj, h, mul_coe, mk_coe]

Premises used: PNat.mul_coe, PNat.coe_inj, PNat.mk_coe
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
rw : (↑k : ℕ) ∣ (↑m : ℕ) ↔ m.mod k = k
⊢ k ∣ m ↔ m.mod k = k

Tactic:
rw [dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
rw : (↑m : ℕ) % (↑k : ℕ) = 0 ↔ m.mod k = k
⊢ (↑k : ℕ) ∣ (↑m : ℕ) ↔ m.mod k = k

Tactic:
rw [Nat.dvd_iff_mod_eq_zero]

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
mp : (↑m : ℕ) % (↑k : ℕ) = 0 → m.mod k = k
mpr : m.mod k = k → (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0 ↔ m.mod k = k

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
mp : (↑(m.mod k) : ℕ) = (↑k : ℕ)
⊢ m.mod k = k

Tactic:
apply PNat.eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
mp : (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) = (↑k : ℕ)
mp₁ mp₂ : (↑k : ℕ) = (↑k : ℕ)
⊢ (↑(m.mod k) : ℕ) = (↑k : ℕ)

Tactic:
rw [mod_coe, if_pos h]

Premises used: PNat.mod_coe, if_pos
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : m.mod k = k
pos : ∀ (h' : (↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) = 0
neg : ∀ (h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
by_cases h' : (m : ℕ) % (k : ℕ) = 0

Premises used: PNat.val
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : m.mod k = k
h' : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
h'
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : m.mod k = k
h' : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
exact h'
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h : m.mod k = k
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑(m.mod k) : ℕ) = (↑k : ℕ)

Tactic:
replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
h : (↑(m.mod k) : ℕ) = (↑k : ℕ)
⊢ (↑m : ℕ) % (↑k : ℕ) = (↑k : ℕ)

Tactic:
rw [mod_coe, if_neg h'] at h

Premises used: PNat.mod_coe, if_neg
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
h : (↑m : ℕ) % (↑k : ℕ) = (↑k : ℕ)
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

Premises used: PNat.val, False.elim, Nat.mod_lt, PNat.pos, LT.lt.ne
-- Module: Mathlib.Data.PNat.Basic
Goal:
k m : ℕ+
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
h : (↑m : ℕ) % (↑k : ℕ) = (↑k : ℕ)
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

Premises used: PNat.val, False.elim, Nat.mod_lt, PNat.pos, LT.lt.ne
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
rw : n.mod m = m → m ≤ n
⊢ m ∣ n → m ≤ n

Tactic:
rw [dvd_iff']

Premises used: PNat.dvd_iff'
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
h : n.mod m = m
rw : n.mod m ≤ n
⊢ m ≤ n

Tactic:
rw [← h]
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n

Tactic:
apply (mod_le n m).left

Premises used: And.left, PNat.mod_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : k ∣ m
a : (↑(k * m.divExact k) : ℕ) = (↑m : ℕ)
⊢ k * m.divExact k = m

Tactic:
apply PNat.eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h : k ∣ m
a : (↑k : ℕ) * (m.div k).succ = (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ)
a₁ : (↑k : ℕ) * (m.div k).succ = (↑k : ℕ) * m.div k + (↑k : ℕ)
a₂ a₃ : (↑k : ℕ) * m.div k + (↑k : ℕ) = (↑k : ℕ) * m.div k + (↑k : ℕ)
⊢ (↑k : ℕ) * (m.div k).succ = (↑m : ℕ)

Tactic:
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]

Premises used: Nat.mul_succ, PNat.div_add_mod, Iff.mp, PNat.dvd_iff'
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ m ∣ n → n ∣ m → m = n

Tactic:
fun hmn hnm =>
  (le_of_dvd hmn).antisymm (le_of_dvd hnm)

Premises used: PNat.le_of_dvd, LE.le.antisymm
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
⊢ n ∣ 1 ↔ n = 1

Tactic:
⟨fun h => dvd_antisymm h (one_dvd n), fun h => h.symm ▸ dvd_refl 1⟩

Premises used: Eq.rec, PNat.dvd_antisymm, one_dvd, Iff.intro, OfNat.ofNat, Eq.symm, dvd_refl
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
a : ℕ
h : a ∣ (↑n : ℕ)
apply : a ≠ 0
⊢ 0 < a

Tactic:
apply pos_iff_ne_zero.2

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
a : ℕ
h : a ∣ (↑n : ℕ)
hzero : a = 0
⊢ 0 ∣ (↑n : ℕ)

Tactic:
rw [hzero] at h
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
a : ℕ
h : a ∣ (↑n : ℕ)
hzero : a = 0
h₁ : 0 ∣ (↑n : ℕ)
⊢ a = 0

Tactic:
rw [hzero] at h
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
a : ℕ
h : 0 ∣ (↑n : ℕ)
hzero : a = 0
⊢ False

Tactic:
PNat.ne_zero n (eq_zero_of_zero_dvd h)

Premises used: PNat.ne_zero, eq_zero_of_zero_dvd
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
a : ℕ
h : 0 ∣ (↑n : ℕ)
hzero : a = 0
⊢ False

Tactic:
exact PNat.ne_zero n (eq_zero_of_zero_dvd h)

Premises used: PNat.ne_zero, eq_zero_of_zero_dvd
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ
h : 0 < n
⊢ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) : ℕ) = n

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ
h : 0 < n
⊢ natPred (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) = n.pred

Tactic:
rfl

Premises used: PNat.val, PNat.natPred, Nat.pred, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ
⊢ (↑n.succPNat : ℕ) = n.succ

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ
⊢ n.succPNat.natPred = n

Tactic:
rfl

Premises used: PNat.natPred, Nat.pred, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ n.natPred.succPNat = n

Tactic:
Subtype.ext <| succ_pred_eq_of_pos n.2

Premises used: Nat.succ_pred_eq_of_pos, Subtype.property, Subtype.ext, PNat
-- Module: Mathlib.Data.PNat.Defs
Goal:
⊢ toPNat' 0 = 1

Tactic:
rfl

Premises used: Nat.toPNat', Nat.succPNat, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m : ℕ
⊢ (↑(m + 1).toPNat' : ℕ) = m + 1

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn ≤ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k hk ↔ n ≤ k

Tactic:
simp
-- Module: Mathlib.Data.PNat.Defs
Goal:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k hk ↔ n < k

Tactic:
simp
-- Module: Mathlib.Data.PNat.Defs
Goal:
n k : ℕ+
⊢ (↑n : ℕ) ≤ (↑k : ℕ) ↔ n ≤ k

Tactic:
Iff.rfl

Premises used: PNat.val, Iff.rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n k : ℕ+
⊢ (↑n : ℕ) < (↑k : ℕ) ↔ n < k

Tactic:
Iff.rfl

Premises used: PNat.val, Iff.rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ 0 < (↑n : ℕ)

Tactic:
n.2

Premises used: PNat.val, Subtype.property
-- Module: Mathlib.Data.PNat.Defs
Goal:
m n : ℕ+
⊢ (↑m : ℕ) = (↑n : ℕ) → m = n

Tactic:
Subtype.ext

Premises used: PNat.val, Subtype.ext, PNat
-- Module: Mathlib.Data.PNat.Defs
Goal:
⊢ Function.Injective val

Tactic:
Subtype.coe_injective

Premises used: PNat.val, Subtype.coe_injective, PNat
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ (↑n : ℕ) ≠ 0

Tactic:
n.2.ne'

Premises used: PNat.val, LT.lt.ne', Subtype.property
-- Module: Mathlib.Data.PNat.Defs
Goal:
a : ℕ+
⊢ NeZero (↑a : ℕ)

Tactic:
⟨a.ne_zero⟩

Premises used: NeZero.mk, PNat.ne_zero
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ
⊢ 0 < n → (↑n.toPNat' : ℕ) = n

Tactic:
succ_pred_eq_of_pos

Premises used: PNat.val, Nat.succ_pred_eq_of_pos
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ (↑n : ℕ).toPNat' = n

Tactic:
eq (toPNat'_coe n.pos)

Premises used: PNat.toPNat'_coe, PNat.pos, PNat.eq
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ 1 ≤ n

Tactic:
n.2

Premises used: Nat.lt, Subtype.property
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℕ+
⊢ ¬n < 1

Tactic:
not_lt_of_ge n.2

Premises used: Subtype.property, not_lt_of_ge
-- Module: Mathlib.Data.PNat.Defs
Goal:
h : LT.lt (α := ℕ) 0 1
⊢ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 1 h = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
⊢ (↑1 : ℕ) = 1

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m : ℕ+
⊢ (↑m : ℕ) = 1 ↔ m = 1

Tactic:
Subtype.coe_injective.eq_iff' one_coe

Premises used: PNat.val, Function.Injective.eq_iff', PNat.one_coe, Subtype.coe_injective, PNat
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
⊢ (↑(k.modDivAux 0 ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) = (↑k : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
n : ℕ
⊢ (↑(k.modDivAux (n + 1) ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) = n + 1

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
cases : ∀ (x : ℕ), (↑(k.modDivAux x ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) = if x = 0 then (↑k : ℕ) else x
⊢ (↑(k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) =
    if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)

Tactic:
cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

Premises used: PNat.val, if_pos, Nat.zero, Nat.succ, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
⊢ (k.modDivAux 0 ((↑m : ℕ) / (↑k : ℕ))).snd = (↑m : ℕ) / (↑k : ℕ) - 1

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) ((↑m : ℕ) / (↑k : ℕ))).snd = (↑m : ℕ) / (↑k : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
m k : ℕ+
cases :
  ∀ (x : ℕ), (k.modDivAux x ((↑m : ℕ) / (↑k : ℕ))).snd = if x = 0 then (↑m : ℕ) / (↑k : ℕ) - 1 else (↑m : ℕ) / (↑k : ℕ)
⊢ (k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).snd =
    if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑m : ℕ) / (↑k : ℕ) - 1 else (↑m : ℕ) / (↑k : ℕ)

Tactic:
cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

Premises used: PNat.val, if_pos, Nat.zero, Nat.succ, rfl
-- Module: Mathlib.Data.PNat.Defs
Goal:
⊢ CanLift ℕ ℕ+ PNat.val fun (n : ℕ) ↦ 0 < n

Tactic:
⟨fun n hn => ⟨Nat.toPNat' n, PNat.toPNat'_coe hn⟩⟩

Premises used: Nat.toPNat', PNat.toPNat'_coe, Exists.intro, CanLift.mk
-- Module: Mathlib.Data.PNat.Defs
Goal:
n : ℤ
hn : 0 < n
rw : (↑(if 0 < n.natAbs then n.natAbs else 1) : ℤ) = n
rw₁ : (↑n.natAbs : ℤ) = n
rw₂ rw₃ : n = n
⊢ (↑(↑n.natAbs.toPNat' : ℕ) : ℤ) = n

Tactic:
rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'),
        Int.natAbs_of_nonneg hn.le]

Premises used: Iff.mpr, Nat.toPNat'_coe, Int.natAbs_pos, LT.lt.le, if_pos, Int.natAbs_of_nonneg, LT.lt.ne'
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ Repr (Multiset Nat.Primes)

Tactic:
infer_instance
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
⊢ Multiset.card (ofPrime p) = 1

Tactic:
rfl

Premises used: Multiset.card, rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ (⇑coeNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ) = toNatMultiset

Tactic:
rfl

Premises used: Multiset.map, rfl, PrimeMultiset.toNatMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ Function.Injective toNatMultiset

Tactic:
Multiset.map_injective Nat.Primes.coe_nat_injective

Premises used: Nat.Primes.coe_nat_injective, Multiset.map_injective, PrimeMultiset, PrimeMultiset.toNatMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
⊢ (ofPrime p).toNatMultiset = {(↑p : ℕ)}

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.cons, Multiset.ofList, rfl, PrimeMultiset.toNatMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
rcases :
  ∀ (val : ℕ) (hp' : Nat.Prime val),
    Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v →
      ∀ (h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ) = p), Nat.Prime p
⊢ Nat.Prime p

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
val : ℕ
hp' : Nat.Prime val
left : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v
h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ) = p
⊢ Nat.Prime p

Tactic:
h_eq ▸ hp'

Premises used: Eq.rec
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
val : ℕ
hp' : Nat.Prime val
left : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v
h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ) = p
⊢ Nat.Prime p

Tactic:
exact h_eq ▸ hp'
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ (⇑coePNatMonoidHom : (a : PrimeMultiset) → Multiset ℕ+) = toPNatMultiset

Tactic:
rfl

Premises used: Multiset.map, PrimeMultiset.toPNatMultiset, rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
⊢ Function.Injective toPNatMultiset

Tactic:
Multiset.map_injective Nat.Primes.coe_pnat_injective

Premises used: Nat.Primes.coe_pnat_injective, PrimeMultiset.toPNatMultiset, Multiset.map_injective, PrimeMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
⊢ (ofPrime p).toPNatMultiset = {(↑p : ℕ+)}

Tactic:
rfl

Premises used: Multiset.map, List.map, PrimeMultiset.toPNatMultiset, Multiset.cons, Multiset.ofList, rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
rcases :
  ∀ (val : ℕ) (hp' : Nat.Prime val),
    Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v →
      ∀ (h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ+) = p), p.Prime
⊢ p.Prime

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
val : ℕ
hp' : Nat.Prime val
left : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v
h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ+) = p
⊢ p.Prime

Tactic:
h_eq ▸ hp'

Premises used: Eq.rec
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
val : ℕ
hp' : Nat.Prime val
left : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp' ∈ v
h_eq : (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) val hp') : ℕ+) = p
⊢ p.Prime

Tactic:
exact h_eq ▸ hp'
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
rw :
  Multiset.map (Subtype.val (p := fun (n : ℕ) ↦ 0 < n) ∘ Nat.Primes.toPNat) v =
    Multiset.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) v
⊢ Multiset.map (Subtype.val (p := fun (n : ℕ) ↦ 0 < n)) (Multiset.map Nat.Primes.toPNat v) =
    Multiset.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) v

Tactic:
rw [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
⊢ Multiset.map (Subtype.val (p := fun (n : ℕ) ↦ 0 < n) ∘ Nat.Primes.toPNat) v =
    Multiset.map (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) v

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
⊢ (↑v.prod : ℕ) = (Multiset.map PNat.val (Multiset.map Nat.Primes.toPNat v)).prod

Tactic:
have h : (v.prod : ℕ) = ((v.map (↑) : Multiset ℕ+).map (↑)).prod :=
    PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : PrimeMultiset
h : (↑v.prod : ℕ) = (Multiset.map PNat.val (Multiset.map Nat.Primes.toPNat v)).prod
⊢ (↑v.prod : ℕ) = v.toNatMultiset.prod

Tactic:
simpa [Multiset.map_map] using h

Premises used: Multiset.map_map
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : Nat.Primes
⊢ (ofPrime p).prod = (↑p : ℕ+)

Tactic:
Multiset.prod_singleton _

Premises used: Multiset.map, List.map, PrimeMultiset.toPNatMultiset, PrimeMultiset.prod, Multiset.prod_singleton, Multiset.cons, Multiset.ofList
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : ℕ+
s : Multiset ℕ
hs : ∀ (p : ℕ), p ∈ s → Nat.Prime p
simp : (∃ (a : ℕ), ∃ (h : a ∈ s), (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a ⋯) : ℕ) = (↑p : ℕ)) ↔ (↑p : ℕ) ∈ s
⊢ p ∈ (ofNatMultiset s hs).toPNatMultiset ↔ (↑p : ℕ) ∈ s

Tactic:
simp only [ofNatMultiset, toPNatMultiset, Multiset.map_pmap, Multiset.mem_pmap, Nat.Primes.toPNat,
    ← PNat.coe_inj]

Premises used: Nat.Primes.toPNat, PrimeMultiset.toPNatMultiset, PrimeMultiset.ofNatMultiset, Multiset.map_pmap, PNat.coe_inj, Multiset.mem_pmap
-- Module: Mathlib.Data.PNat.Factors
Goal:
p : ℕ+
s : Multiset ℕ
hs : ∀ (p : ℕ), p ∈ s → Nat.Prime p
⊢ (∃ (a : ℕ), ∃ (h : a ∈ s), (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a ⋯) : ℕ) = (↑p : ℕ)) ↔ (↑p : ℕ) ∈ s

Tactic:
simp
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
rw :
  Multiset.pmap (p := Nat.Prime)
      (fun (a : ℕ) (h : Nat.Prime a) ↦ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) a h) : ℕ)) v h =
    v
rw₁ : Multiset.map (fun (a : ℕ) ↦ a) v = v
rw₂ rw₃ : v = v
⊢ Multiset.map (α := Nat.Primes) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p))
      (Multiset.pmap (p := Nat.Prime)
        (fun (p : ℕ) (hp : Nat.Prime p) ↦ Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) v h) =
    v

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

Premises used: Multiset.pmap_eq_map, Multiset.map_pmap, Multiset.map_id'
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
rw : (ofNatMultiset v h).toNatMultiset.prod = v.prod
rw₁ rw₂ : v.prod = v.prod
⊢ (↑(ofNatMultiset v h).prod : ℕ) = v.prod

Tactic:
rw [coe_prod, to_ofNatMultiset]

Premises used: PrimeMultiset.to_ofNatMultiset, PrimeMultiset.coe_prod
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
h₁ : ∀ (p : ℕ+) (h : p.Prime), (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) = id p
⊢ 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:
funext p h
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h_1 : ∀ (p : ℕ+), p ∈ v → p.Prime
p : ℕ+
h : p.Prime
h₁ : (↑(↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) : ℕ) = (↑(id p) : ℕ)
⊢ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) = id p

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.PNat.Factors
Goal:
v : Multiset ℕ+
h_1 : ∀ (p : ℕ+), p ∈ v → p.Prime
p : ℕ+
h : p.Prime
⊢ (↑(↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) : ℕ) = (↑(id p) : ℕ)

Tactic:
rfl