awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
h : ¬b < a
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = 1
have neg : (↑(toPNat' 0) : ℕ) = 1
Tactic: rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
⊢ a - b ≤ a
have rw : (if b < a then (↑a : ℕ) - (↑b : ℕ) else 1) ≤ (↑a : ℕ)
Tactic: rw [← coe_le_coe, sub_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
⊢ (if b < a then (↑a : ℕ) - (↑b : ℕ) else 1) ≤ (↑a : ℕ)
have pos : ∀ (h : b < a), (↑a : ℕ) - (↑b : ℕ) ≤ (↑a : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
pos : ∀ (h : b < a), (↑a : ℕ) - (↑b : ℕ) ≤ (↑a : ℕ)
⊢ (if b < a then (↑a : ℕ) - (↑b : ℕ) else 1) ≤ (↑a : ℕ)
have neg : ∀ (h : ¬b < a), 1 ≤ (↑a : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
hab : a < b
⊢ a ≤ b - 1
have rw : (↑a : ℕ) ≤ if 1 < b then (↑b : ℕ) - (↑1 : ℕ) else 1
Tactic: rw [← coe_le_coe, sub_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
hab : a < b
⊢ (↑a : ℕ) ≤ if 1 < b then (↑b : ℕ) - (↑1 : ℕ) else 1
have pos : ∀ (h : 1 < b), (↑a : ℕ) ≤ (↑b : ℕ) - (↑1 : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
hab : a < b
pos : ∀ (h : 1 < b), (↑a : ℕ) ≤ (↑b : ℕ) - (↑1 : ℕ)
⊢ (↑a : ℕ) ≤ if 1 < b then (↑b : ℕ) - (↑1 : ℕ) else 1
have neg : ∀ (h : ¬1 < b), (↑a : ℕ) ≤ 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
h : a < b
⊢ (↑(a + (b - a)) : ℕ) = (↑b : ℕ)
have rw : (↑a : ℕ) + ((↑b : ℕ) - (↑a : ℕ)) = (↑b : ℕ)
Tactic: rw [add_coe, sub_coe, if_pos h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
h : b < a
⊢ a - b + b = a
have rw : b + (a - b) = a
Tactic: rw [add_comm, add_sub_of_lt h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
h : b < a
rw : b + (a - b) = a
⊢ a - b + b = a
have rw₁ : a = a
Tactic: rw [add_comm, add_sub_of_lt h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
⊢ (↑(k.modDivAux 0 (q + 1)).1 : ℕ) + (↑k : ℕ) * (k.modDivAux 0 (q + 1)).2 = 0 + (↑k : ℕ) * (q + 1)
have change : (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
Tactic: change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
⊢ (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
have rw : (↑k : ℕ) + (↑k : ℕ) * q = 0 + (↑k : ℕ) * (q + 1)
Tactic: rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
rw : (↑k : ℕ) + (↑k : ℕ) * q = 0 + (↑k : ℕ) * (q + 1)
⊢ (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
have rw₁ : (↑k : ℕ) + (↑k : ℕ) * q = 0 + ((↑k : ℕ) * q + (↑k : ℕ))
Tactic: rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
rw : (↑k : ℕ) + (↑k : ℕ) * q = 0 + (↑k : ℕ) * (q + 1)
rw₁ : (↑k : ℕ) + (↑k : ℕ) * q = 0 + ((↑k : ℕ) * q + (↑k : ℕ))
⊢ (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
have rw₂ : (↑k : ℕ) + (↑k : ℕ) * q = (↑k : ℕ) * q + (↑k : ℕ)
Tactic: rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
rw : (↑k : ℕ) + (↑k : ℕ) * q = 0 + (↑k : ℕ) * (q + 1)
rw₁ : (↑k : ℕ) + (↑k : ℕ) * q = 0 + ((↑k : ℕ) * q + (↑k : ℕ))
rw₂ : (↑k : ℕ) + (↑k : ℕ) * q = (↑k : ℕ) * q + (↑k : ℕ)
⊢ (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
have rw₃ : (↑k : ℕ) * q + (↑k : ℕ) = (↑k : ℕ) * q + (↑k : ℕ)
Tactic: rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ False
have h₁ : 0 = (↑m : ℕ)
Tactic: rw [hr, hq, mul_zero, zero_add] at h₀
Cleared hypotheses: h₀, hr, hq
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)
have this : ¬((↑m : ℕ) % (↑k : ℕ) = 0 ∧ (↑m : ℕ) / (↑k : ℕ) = 0)
Tactic: have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) := by
    rintro ⟨hr, hq⟩
    rw [hr, hq, mul_zero, zero_add] at h₀
    exact (m.ne_zero h₀.symm).elim
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
this : ¬((↑m : ℕ) % (↑k : ℕ) = 0 ∧ (↑m : ℕ) / (↑k : ℕ) = 0)
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)
have this₁ : (↑(k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).1 : ℕ) +
    (↑k : ℕ) * (k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).2 =
  (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
Tactic: have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
⊢ (↑(m.mod k) : ℕ) + m.div k * (↑k : ℕ) = (↑m : ℕ)
have rw : (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
⊢ m.div k * (↑k : ℕ) + (↑(m.mod k) : ℕ) = (↑m : ℕ)
have rw : (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ) = (↑m : ℕ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
⊢ (↑(m.mod k) : ℕ) ≤ (↑m : ℕ) ∧ (↑(m.mod k) : ℕ) ≤ (↑k : ℕ)
have rw : (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑m : ℕ) ∧
  (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑k : ℕ)
Tactic: rw [mod_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
⊢ (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑m : ℕ) ∧
    (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑k : ℕ)
have pos : ∀ (h : (↑m : ℕ) % (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
pos : ∀ (h : (↑m : ℕ) % (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
⊢ (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑m : ℕ) ∧
    (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) ≤ (↑k : ℕ)
have neg : ∀ (h : ¬(↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑m : ℕ) % (↑k : ℕ) ≤ (↑k : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have hm : (↑m : ℕ) > 0
Tactic: have hm : (m : ℕ) > 0 := m.pos
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑m : ℕ) > 0
⊢ (↑k : ℕ) ≤ (↑m : ℕ) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have pos : ∀ (hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
Tactic: rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have pos : ∀ (h₁ : (↑m : ℕ) / (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
Tactic: by_cases h₁ : (m : ℕ) / (k : ℕ) = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
pos : ∀ (h₁ : (↑m : ℕ) / (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have neg : ∀ (h₁ : ¬(↑m : ℕ) / (↑k : ℕ) = 0), (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
Tactic: by_cases h₁ : (m : ℕ) / (k : ℕ) = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
m k : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
hm : (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) > 0
h₁ : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have hm₁ : GT.gt (α := ℕ) 0 0
Tactic: rw [h₁, mul_zero] at hm
Cleared hypotheses: hm, h₁
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
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 : ℕ)) ∧ (↑k : ℕ) ≤ (↑k : ℕ)
have h₃ : (↑k : ℕ) ≤ (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
Tactic: rw [mul_one] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
⊢ k ∣ m ↔ (↑k : ℕ) ∣ (↑m : ℕ)
have mp : k ∣ m → (↑k : ℕ) ∣ (↑m : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
mp : k ∣ m → (↑k : ℕ) ∣ (↑m : ℕ)
⊢ k ∣ m ↔ (↑k : ℕ) ∣ (↑m : ℕ)
have mpr : (↑k : ℕ) ∣ (↑m : ℕ) → k ∣ m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : k ∣ m
⊢ (↑k : ℕ) ∣ (↑m : ℕ)
have mp : ∀ (w : ℕ+), (↑k : ℕ) ∣ (↑(k * w) : ℕ)
Tactic: rcases h with ⟨_, rfl⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : (↑k : ℕ) ∣ (↑m : ℕ)
⊢ k ∣ m
have mpr : ∀ (a : ℕ) (h : (↑m : ℕ) = (↑k : ℕ) * a), k ∣ m
Tactic: rcases h with ⟨a, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
a : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * a
⊢ k ∣ m
have mpr : ∀ (n : ℕ) (h : (↑m : ℕ) = (↑k : ℕ) * n.succ), 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
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
n : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * n.succ
⊢ k ∣ m
have h₁ : m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ sorry
Tactic: use ⟨n.succ, n.succ_pos⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
n : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * n.succ
⊢ m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯
have h₁ : (↑m : ℕ) = (↑(k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ sorry) : ℕ)
Tactic: rw [← coe_inj, h, mul_coe, mk_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
n : ℕ
h : (↑m : ℕ) = (↑k : ℕ) * n.succ
h₁ : (↑m : ℕ) = (↑(k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯) : ℕ)
⊢ m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯
have h₂ : (↑k : ℕ) * n.succ = (↑(k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ sorry) : ℕ)
Tactic: rw [← coe_inj, h, mul_coe, mk_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
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 ⋯) : ℕ)
⊢ m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯
have h₃ : (↑k : ℕ) * n.succ = (↑k : ℕ) * (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ sorry) : ℕ)
Tactic: rw [← coe_inj, h, mul_coe, mk_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
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 ⋯) : ℕ)
⊢ m = k * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n.succ ⋯
have h₄ : (↑k : ℕ) * n.succ = (↑k : ℕ) * n.succ
Tactic: rw [← coe_inj, h, mul_coe, mk_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k
have rw : (↑k : ℕ) ∣ (↑m : ℕ) ↔ m.mod k = k
Tactic: rw [dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
⊢ (↑k : ℕ) ∣ (↑m : ℕ) ↔ m.mod k = k
have rw : (↑m : ℕ) % (↑k : ℕ) = 0 ↔ m.mod k = k
Tactic: rw [Nat.dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
⊢ (↑m : ℕ) % (↑k : ℕ) = 0 ↔ m.mod k = k
have mp : (↑m : ℕ) % (↑k : ℕ) = 0 → m.mod k = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
mp : (↑m : ℕ) % (↑k : ℕ) = 0 → m.mod k = k
⊢ (↑m : ℕ) % (↑k : ℕ) = 0 ↔ m.mod k = k
have mpr : m.mod k = k → (↑m : ℕ) % (↑k : ℕ) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ m.mod k = k
have mp : (↑(m.mod k) : ℕ) = (↑k : ℕ)
Tactic: apply PNat.eq
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑(m.mod k) : ℕ) = (↑k : ℕ)
have mp : (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) = (↑k : ℕ)
Tactic: rw [mod_coe, if_pos h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : (↑m : ℕ) % (↑k : ℕ) = 0
mp : (if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)) = (↑k : ℕ)
⊢ (↑(m.mod k) : ℕ) = (↑k : ℕ)
have mp₁ : (↑k : ℕ) = (↑k : ℕ)
Tactic: rw [mod_coe, if_pos h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : m.mod k = k
⊢ (↑m : ℕ) % (↑k : ℕ) = 0
have pos : ∀ (h' : (↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) = 0
Tactic: by_cases h' : (m : ℕ) % (k : ℕ) = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
k m : ℕ+
h : m.mod k = k
pos : ∀ (h' : (↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0
have neg : ∀ (h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0), (↑m : ℕ) % (↑k : ℕ) = 0
Tactic: by_cases h' : (m : ℕ) % (k : ℕ) = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
k m : ℕ+
h : m.mod k = k
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) % (↑k : ℕ) = 0
have h₁ : (↑(m.mod k) : ℕ) = (↑k : ℕ)
Tactic: replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
k m : ℕ+
h' : ¬(↑m : ℕ) % (↑k : ℕ) = 0
h : (↑(m.mod k) : ℕ) = (↑k : ℕ)
⊢ (↑m : ℕ) % (↑k : ℕ) = 0
have h₁ : (↑m : ℕ) % (↑k : ℕ) = (↑k : ℕ)
Tactic: rw [mod_coe, if_neg h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m n : ℕ+
⊢ m ∣ n → m ≤ n
have rw : n.mod m = m → m ≤ n
Tactic: rw [dvd_iff']
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m n : ℕ+
h : n.mod m = m
⊢ m ≤ n
have rw : n.mod m ≤ n
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : k ∣ m
⊢ k * m.divExact k = m
have a : (↑(k * m.divExact k) : ℕ) = (↑m : ℕ)
Tactic: apply PNat.eq
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : k ∣ m
⊢ (↑k : ℕ) * (m.div k).succ = (↑m : ℕ)
have a : (↑k : ℕ) * (m.div k).succ = (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ)
Tactic: rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
m k : ℕ+
h : k ∣ m
a : (↑k : ℕ) * (m.div k).succ = (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ)
⊢ (↑k : ℕ) * (m.div k).succ = (↑m : ℕ)
have a₁ : (↑k : ℕ) * (m.div k).succ = (↑k : ℕ) * m.div k + (↑k : ℕ)
Tactic: rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
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 : ℕ)
⊢ (↑k : ℕ) * (m.div k).succ = (↑m : ℕ)
have a₂ : (↑k : ℕ) * m.div k + (↑k : ℕ) = (↑k : ℕ) * m.div k + (↑k : ℕ)
Tactic: rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
n : ℕ+
a : ℕ
h : a ∣ (↑n : ℕ)
⊢ 0 < a
have apply : a ≠ 0
Tactic: apply pos_iff_ne_zero.2
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (hypothesis)
Goal:
n : ℕ+
a : ℕ
h : a ∣ (↑n : ℕ)
hzero : a = 0
⊢ False
have h₁ : 0 ∣ (↑n : ℕ)
Tactic: rw [hzero] at h
Cleared hypotheses: h, hzero
-- Lean 4 proof step from Mathlib.Data.PNat.Defs (goal)
Goal:
m k : ℕ+
⊢ (↑(k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) =
    if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑k : ℕ) else (↑m : ℕ) % (↑k : ℕ)
have cases : ∀ (x : ℕ), (↑(k.modDivAux x ((↑m : ℕ) / (↑k : ℕ))).fst : ℕ) = if x = 0 then (↑k : ℕ) else x
Tactic: cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl
-- Lean 4 proof step from Mathlib.Data.PNat.Defs (goal)
Goal:
m k : ℕ+
⊢ (k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).snd =
    if (↑m : ℕ) % (↑k : ℕ) = 0 then (↑m : ℕ) / (↑k : ℕ) - 1 else (↑m : ℕ) / (↑k : ℕ)
have cases : ∀ (x : ℕ), (k.modDivAux x ((↑m : ℕ) / (↑k : ℕ))).snd = if x = 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
-- Lean 4 proof step from Mathlib.Data.PNat.Defs (goal)
Goal:
n : ℤ
hn : 0 < n
⊢ (↑(↑n.natAbs.toPNat' : ℕ) : ℤ) = n
have rw : (↑(if 0 < n.natAbs then n.natAbs else 1) : ℤ) = n
Tactic: rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'),
        Int.natAbs_of_nonneg hn.le]
-- Lean 4 proof step from Mathlib.Data.PNat.Defs (goal)
Goal:
n : ℤ
hn : 0 < n
rw : (↑(if 0 < n.natAbs then n.natAbs else 1) : ℤ) = n
⊢ (↑(↑n.natAbs.toPNat' : ℕ) : ℤ) = n
have rw₁ : (↑n.natAbs : ℤ) = n
Tactic: rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'),
        Int.natAbs_of_nonneg hn.le]
-- Lean 4 proof step from Mathlib.Data.PNat.Defs (goal)
Goal:
n : ℤ
hn : 0 < n
rw : (↑(if 0 < n.natAbs then n.natAbs else 1) : ℤ) = n
rw₁ : (↑n.natAbs : ℤ) = n
⊢ (↑(↑n.natAbs.toPNat' : ℕ) : ℤ) = n
have rw₂ : n = n
Tactic: rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'),
        Int.natAbs_of_nonneg hn.le]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
⊢ Nat.Prime p
have 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
Tactic: rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
⊢ p.Prime
have 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
Tactic: rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : PrimeMultiset
⊢ 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
have 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
Tactic: rw [Multiset.map_map]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
v : PrimeMultiset
⊢ (↑v.prod : ℕ) = v.toNatMultiset.prod
have h : (↑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
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
p : ℕ+
s : Multiset ℕ
hs : ∀ (p : ℕ), p ∈ s → Nat.Prime p
⊢ p ∈ (ofNatMultiset s hs).toPNatMultiset ↔ (↑p : ℕ) ∈ s
have simp : (∃ (a : ℕ), ∃ (h : a ∈ s), (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a sorry) : ℕ) = (↑p : ℕ)) ↔ (↑p : ℕ) ∈ s
Tactic: simp only [ofNatMultiset, toPNatMultiset, Multiset.map_pmap, Multiset.mem_pmap, Nat.Primes.toPNat,
    ← PNat.coe_inj]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ 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
have 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
Tactic: rw [Multiset.map_pmap, Multiset.pmap_eq_map, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ 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
have rw₁ : Multiset.map (fun (a : ℕ) ↦ a) v = v
Tactic: rw [Multiset.map_pmap, Multiset.pmap_eq_map, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
⊢ 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
have rw₂ : v = v
Tactic: rw [Multiset.map_pmap, Multiset.pmap_eq_map, Multiset.map_id']
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ (↑(ofNatMultiset v h).prod : ℕ) = v.prod
have rw : (ofNatMultiset v h).toNatMultiset.prod = v.prod
Tactic: rw [coe_prod, to_ofNatMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
Goal:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
rw : (ofNatMultiset v h).toNatMultiset.prod = v.prod
⊢ (↑(ofNatMultiset v h).prod : ℕ) = v.prod
have rw₁ : v.prod = v.prod
Tactic: rw [coe_prod, to_ofNatMultiset]
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
have h₁ : ∀ (p : ℕ+) (h : p.Prime), (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) = id p
Tactic: funext p h
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (goal)
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
have h₁ : (↑(↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑p : ℕ) h) : ℕ+) : ℕ) = (↑(id p) : ℕ)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.PNat.Factors (hypothesis)
Goal:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ 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 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
Tactic: have : (fun (p : ℕ+) (h : p.Prime) => ((↑) : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p := by
    funext p h
    apply Subtype.ext
    rfl
-- 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
⊢ 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 (a : ℕ+) (h : a.Prime) ↦ (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) (↑a : ℕ) h) : ℕ+)) v h =
  v
Tactic: rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]