awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ Function.Injective natPred

Tactic:
natPred_strictMono.injective

Premises used: StrictMono.injective, PNat.natPred_strictMono
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ m.natPred < n.natPred ↔ m < n

Tactic:
natPred_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, PNat.natPred_strictMono
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ m.natPred ≤ n.natPred ↔ m ≤ n

Tactic:
natPred_strictMono.le_iff_le

Premises used: PNat.natPred_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ m.natPred = n.natPred ↔ m = n

Tactic:
natPred_injective.eq_iff

Premises used: PNat.natPred_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ (↑(OfNat.ofNat n) : ℕ) = OfNat.ofNat n

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ StrictMono succPNat

Tactic:
fun _ _ => Nat.succ_lt_succ

Premises used: StrictMono, Nat.succ_lt_succ
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ Monotone succPNat

Tactic:
succPNat_strictMono.monotone

Premises used: StrictMono.monotone, Nat.succPNat_strictMono
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ
⊢ m.succPNat < n.succPNat ↔ m < n

Tactic:
succPNat_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Nat.succPNat_strictMono
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ
⊢ m.succPNat ≤ n.succPNat ↔ m ≤ n

Tactic:
succPNat_strictMono.le_iff_le

Premises used: Nat.succPNat_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ Function.Injective succPNat

Tactic:
succPNat_strictMono.injective

Premises used: Nat.succPNat_strictMono, StrictMono.injective
-- Module: Mathlib.Data.PNat.Basic
Goal:
n m : ℕ
⊢ n.succPNat = m.succPNat ↔ n = m

Tactic:
succPNat_injective.eq_iff

Premises used: Function.Injective.eq_iff, Nat.succPNat_injective
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ (↑m : ℕ) = (↑n : ℕ) ↔ m = n

Tactic:
Subtype.ext_iff.symm

Premises used: PNat.val, Subtype.ext_iff, Iff.symm, PNat
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ (↑(m + n) : ℕ) = (↑m : ℕ) + (↑n : ℕ)

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ (⇑OrderIso.pnatIsoNat.symm : (a : ℕ) → ℕ+) = succPNat

Tactic:
rfl

Premises used: Nat.succPNat, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
⊢ a < b + 1 ↔ a ≤ b

Tactic:
Nat.lt_add_one_iff

Premises used: Nat.lt_add_one_iff
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
⊢ a + 1 ≤ b ↔ a < b

Tactic:
Nat.add_one_le_iff

Premises used: Nat.add_one_le_iff
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ Eq (α := ℕ+) ⊥ 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
apply : (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k
⊢ p a

Tactic:
apply strongInductionOn a

Premises used: PNat.strongInductionOn
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop → p m
zero :
  (kprop : LT.lt (α := ℕ) 0 0) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop)
succ :
  (k : ℕ) →
    (kprop : 0 < k + 1) →
      (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop → p m) →
        p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop)

Tactic:
rcases k with - | k
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : LT.lt (α := ℕ) 0 0
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop → p m
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop)

Tactic:
exact (lt_irrefl 0 kprop).elim

Premises used: lt_irrefl, False.elim, OfNat.ofNat
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop → p m
succ :
  (kprop : 0 < HAdd.hAdd (α := ℕ) 0 1) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop)
succ₁ :
  (k : ℕ) →
    (kprop : 0 < k + 1 + 1) →
      (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop → p m) →
        p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop)

Tactic:
rcases k with - | k
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < HAdd.hAdd (α := ℕ) 0 1
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop → p m
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop)

Tactic:
exact hz
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1 + 1
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop → p m
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop)

Tactic:
exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (Nat.lt_succ_iff.2 hm)

Premises used: Iff.mpr, Subtype.mk, Nat.lt_succ_iff, Nat.succ_pos, Nat.succ
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
rcases : (n : ℕ) → (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
⊢ p n

Tactic:
rcases n with ⟨n, h⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : LT.lt (α := ℕ) 0 0
⊢ ¬LT.lt (α := ℕ) 0 0

Tactic:
decide
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : LT.lt (α := ℕ) 0 0
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)

Tactic:
exact absurd h (by decide)

Premises used: absurd
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
h : 0 < n + 1
succ₁ :
  (IH : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)) →
    (h : 0 < HAdd.hAdd (α := ℕ) 0 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) h)
succ₂ :
  (n : ℕ) →
    (IH : (h : 0 < n + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)) →
      (h : 0 < n + 1 + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1 + 1) h)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
IH : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
h : 0 < HAdd.hAdd (α := ℕ) 0 1
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) h)

Tactic:
exact one
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
h : 0 < n + 1 + 1
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1 + 1) h)

Tactic:
exact succ _ (IH n.succ_pos)

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
succ₁ :
  (n : ℕ) →
    (IH : (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)) →
      (h : 0 < n + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)

Tactic:
induction n with
  | zero => exact absurd h (by decide)
  | succ n IH =>
    rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)

Premises used: absurd, Nat.zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ recOn 1 (p := p) one succ = one

Tactic:
rfl

Premises used: PNat.recOn, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
obtain :
  ∀ (n : ℕ) (h : 0 < n),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
⊢ (n + 1).recOn (p := p) one succ = succ n (n.recOn (p := p) one succ)

Tactic:
obtain ⟨n, h⟩ := n
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero :
  ∀ (h : LT.lt (α := ℕ) 0 0),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
succ₁ :
  ∀ (n : ℕ) (h : 0 < n + 1),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))

Tactic:
cases n
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : LT.lt (α := ℕ) 0 0
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))

Tactic:
exact absurd h (by decide)

Premises used: absurd
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n + 1
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero :
  ∀ (h : LT.lt (α := ℕ) 0 0),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
succ₁ :
  ∀ (n : ℕ) (h : 0 < n + 1),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))
zero₁ :
  ∀ (h : LT.lt (α := ℕ) 0 0),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
succ₂ :
  ∀ (n : ℕ) (h : 0 < n + 1),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))

Tactic:
cases n <;> [exact absurd h (by decide); rfl]

Premises used: absurd
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ
inst : NeZero m
inst_1 : NeZero n
⊢ LE.le (α := ℕ+) (OfNat.ofNat m) (OfNat.ofNat n) ↔ LE.le (α := ℕ) (OfNat.ofNat m) (OfNat.ofNat n)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ
inst : NeZero m
inst_1 : NeZero n
⊢ LT.lt (α := ℕ+) (OfNat.ofNat m) (OfNat.ofNat n) ↔ LT.lt (α := ℕ) (OfNat.ofNat m) (OfNat.ofNat n)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ
inst : NeZero m
inst_1 : NeZero n
⊢ Eq (α := ℕ+) (OfNat.ofNat m) (OfNat.ofNat n) ↔ Eq (α := ℕ) (OfNat.ofNat m) (OfNat.ofNat n)

Tactic:
Subtype.mk_eq_mk

Premises used: Subtype.mk_eq_mk, PNat
-- Module: Mathlib.Data.PNat.Basic
Goal:
m n : ℕ+
⊢ (↑(m * n) : ℕ) = (↑m : ℕ) * (↑n : ℕ)

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ (⇑coeMonoidHom : (a : ℕ+) → ℕ) = val

Tactic:
rfl

Premises used: PNat.val, rfl, PNat
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
⊢ n ≤ 1 ↔ n = 1

Tactic:
simp
-- Module: Mathlib.Data.PNat.Basic
Goal:
n m : ℕ+
⊢ n < m + n

Tactic:
lt_add_of_pos_left _ m.2

Premises used: lt_add_of_pos_left, Subtype.property
-- Module: Mathlib.Data.PNat.Basic
Goal:
n m : ℕ+
⊢ n < n + m

Tactic:
(lt_add_left n m).trans_eq (add_comm _ _)

Premises used: LT.lt.trans_eq, add_comm, PNat.lt_add_left
-- Module: Mathlib.Data.PNat.Basic
Goal:
m : ℕ+
n : ℕ
⊢ (↑(m ^ n) : ℕ) = (↑m : ℕ) ^ n

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
⊢ 1 < b

Tactic:
hab.one_lt

Premises used: LT.lt.one_lt
-- Module: Mathlib.Data.PNat.Basic
Goal:
a : ℕ+
⊢ a + 1 = (↑a : ℕ).succPNat

Tactic:
rfl

Premises used: PNat.val, Nat.succPNat, rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
a : ℕ+
⊢ a < (↑a : ℕ).succPNat

Tactic:
Nat.lt_add_one a

Premises used: PNat.val, Nat.lt_add_one
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
pos : ∀ (h : b < a), (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = (↑a : ℕ) - (↑b : ℕ)
neg : ∀ (h : ¬b < a), (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = 1
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = if b < a then (↑a : ℕ) - (↑b : ℕ) else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : b < a
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = (↑a : ℕ) - (↑b : ℕ)

Tactic:
toPNat'_coe (tsub_pos_of_lt h)

Premises used: PNat.toPNat'_coe, tsub_pos_of_lt
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : b < a
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = (↑a : ℕ) - (↑b : ℕ)

Tactic:
exact toPNat'_coe (tsub_pos_of_lt h)

Premises used: PNat.toPNat'_coe, tsub_pos_of_lt
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : ¬b < a
neg : (↑(toPNat' 0) : ℕ) = 1
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = 1

Tactic:
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]

Premises used: Iff.mpr, le_of_not_gt, tsub_eq_zero_iff_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : ¬b < a
⊢ (↑(toPNat' 0) : ℕ) = 1

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
rw : (if b < a then (↑a : ℕ) - (↑b : ℕ) else 1) ≤ (↑a : ℕ)
⊢ a - b ≤ a

Tactic:
rw [← coe_le_coe, sub_coe]

Premises used: PNat.sub_coe, PNat.coe_le_coe
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
pos : ∀ (h : b < a), (↑a : ℕ) - (↑b : ℕ) ≤ (↑a : ℕ)
neg : ∀ (h : ¬b < a), 1 ≤ (↑a : ℕ)
⊢ (if b < a then (↑a : ℕ) - (↑b : ℕ) else 1) ≤ (↑a : ℕ)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : b < a
⊢ (↑a : ℕ) - (↑b : ℕ) ≤ (↑a : ℕ)

Tactic:
Nat.sub_le a b

Premises used: PNat.val, Nat.sub_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : b < a
⊢ (↑a : ℕ) - (↑b : ℕ) ≤ (↑a : ℕ)

Tactic:
exact Nat.sub_le a b

Premises used: PNat.val, Nat.sub_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ (↑a : ℕ)

Tactic:
a.2

Premises used: PNat.val, Nat.lt, Subtype.property
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ (↑a : ℕ)

Tactic:
exact a.2

Premises used: Subtype.property
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
rw : (↑a : ℕ) ≤ if 1 < b then (↑b : ℕ) - (↑1 : ℕ) else 1
⊢ a ≤ b - 1

Tactic:
rw [← coe_le_coe, sub_coe]

Premises used: PNat.sub_coe, PNat.coe_le_coe
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
pos : ∀ (h : 1 < b), (↑a : ℕ) ≤ (↑b : ℕ) - (↑1 : ℕ)
neg : ∀ (h : ¬1 < b), (↑a : ℕ) ≤ 1
⊢ (↑a : ℕ) ≤ if 1 < b then (↑b : ℕ) - (↑1 : ℕ) else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
h : 1 < b
⊢ (↑a : ℕ) ≤ (↑b : ℕ) - (↑1 : ℕ)

Tactic:
Nat.le_pred_of_lt hab

Premises used: Nat.le_pred_of_lt, Nat.pred
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
h : 1 < b
⊢ (↑a : ℕ) ≤ (↑b : ℕ) - (↑1 : ℕ)

Tactic:
exact Nat.le_pred_of_lt hab

Premises used: Nat.le_pred_of_lt
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ (↑a : ℕ) ≤ 1

Tactic:
hab.le.trans (le_of_not_gt h)

Premises used: PNat.val, le_of_not_gt, LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ (↑a : ℕ) ≤ 1

Tactic:
exact hab.le.trans (le_of_not_gt h)

Premises used: le_of_not_gt, LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : a < b
rw : (↑a : ℕ) + ((↑b : ℕ) - (↑a : ℕ)) = (↑b : ℕ)
⊢ (↑(a + (b - a)) : ℕ) = (↑b : ℕ)

Tactic:
rw [add_coe, sub_coe, if_pos h]

Premises used: PNat.sub_coe, PNat.add_coe, if_pos
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : a < b
⊢ (↑a : ℕ) + ((↑b : ℕ) - (↑a : ℕ)) = (↑b : ℕ)

Tactic:
add_tsub_cancel_of_le h.le

Premises used: LT.lt.le, add_tsub_cancel_of_le
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : a < b
⊢ (↑a : ℕ) + ((↑b : ℕ) - (↑a : ℕ)) = (↑b : ℕ)

Tactic:
exact add_tsub_cancel_of_le h.le
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
h : b < a
rw : b + (a - b) = a
rw₁ rw₂ : a = a
⊢ a - b + b = a

Tactic:
rw [add_comm, add_sub_of_lt h]

Premises used: add_comm, PNat.add_sub_of_lt
-- Module: Mathlib.Data.PNat.Basic
Goal:
a b : ℕ+
⊢ a + b - b = a

Tactic:
add_right_cancel (sub_add_of_lt (lt_add_left _ _))

Premises used: PNat.sub_add_of_lt, add_right_cancel, PNat.lt_add_left
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ
property : 0 < n + 2
h : Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 2) property ≠ 1
⊢ 0 < n + 1

Tactic:
simp
-- Module: Mathlib.Data.PNat.Basic
Goal:
k : ℕ+
q : ℕ
h : ¬(Eq (α := ℕ) 0 0 ∧ q + 1 = 0)
change : (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)
⊢ (↑(k.modDivAux 0 (q + 1)).1 : ℕ) + (↑k : ℕ) * (k.modDivAux 0 (q + 1)).2 = 0 + (↑k : ℕ) * (q + 1)

Tactic:
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)

Premises used: PNat.val, HAdd.hAdd, OfNat.ofNat, Nat.pred
-- Module: Mathlib.Data.PNat.Basic
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 : ℕ)
rw₃ rw₄ : (↑k : ℕ) * q + (↑k : ℕ) = (↑k : ℕ) * q + (↑k : ℕ)
⊢ (↑k : ℕ) + (↑k : ℕ) * (q + 1).pred = 0 + (↑k : ℕ) * (q + 1)

Tactic:
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]

Premises used: Nat.mul_succ, zero_add, add_comm, Nat.pred_succ
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ 0 = (↑m : ℕ)

Tactic:
rw [hr, hq, mul_zero, zero_add] at h₀

Premises used: zero_add, MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
h₁ : 0 = (↑m : ℕ)
⊢ (↑m : ℕ) % (↑k : ℕ) = 0

Tactic:
rw [hr, hq, mul_zero, zero_add] at h₀

Premises used: zero_add, MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
h₁ : 0 = (↑m : ℕ)
hr₁ : (↑m : ℕ) % (↑k : ℕ) = 0
⊢ (↑m : ℕ) / (↑k : ℕ) = 0

Tactic:
rw [hr, hq, mul_zero, zero_add] at h₀

Premises used: zero_add, MulZeroClass.mul_zero
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : 0 = (↑m : ℕ)
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ False

Tactic:
(m.ne_zero h₀.symm).elim

Premises used: False.elim, PNat.ne_zero, Eq.symm
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : 0 = (↑m : ℕ)
hr : (↑m : ℕ) % (↑k : ℕ) = 0
hq : (↑m : ℕ) / (↑k : ℕ) = 0
⊢ False

Tactic:
exact (m.ne_zero h₀.symm).elim

Premises used: False.elim, PNat.ne_zero, Eq.symm
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
⊢ ¬((↑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
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
this : ¬((↑m : ℕ) % (↑k : ℕ) = 0 ∧ (↑m : ℕ) / (↑k : ℕ) = 0)
⊢ (↑(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
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
this_1 : ¬((↑m : ℕ) % (↑k : ℕ) = 0 ∧ (↑m : ℕ) / (↑k : ℕ) = 0)
this :
  (↑(k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).1 : ℕ) +
      (↑k : ℕ) * (k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).2 =
    (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)

Tactic:
this.trans h₀

Premises used: PNat.div, PNat.mod, Eq.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
h₀ : (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ)) = (↑m : ℕ) := ⋯
this_1 : ¬((↑m : ℕ) % (↑k : ℕ) = 0 ∧ (↑m : ℕ) / (↑k : ℕ) = 0)
this :
  (↑(k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).1 : ℕ) +
      (↑k : ℕ) * (k.modDivAux ((↑m : ℕ) % (↑k : ℕ)) ((↑m : ℕ) / (↑k : ℕ))).2 =
    (↑m : ℕ) % (↑k : ℕ) + (↑k : ℕ) * ((↑m : ℕ) / (↑k : ℕ))
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)

Tactic:
exact this.trans h₀

Premises used: Eq.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
⊢ (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ) = (↑m : ℕ)

Tactic:
(add_comm _ _).trans (mod_add_div _ _)

Premises used: PNat.mod_add_div, add_comm, Eq.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
rw : (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)
⊢ (↑(m.mod k) : ℕ) + m.div k * (↑k : ℕ) = (↑m : ℕ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)

Tactic:
mod_add_div _ _

Premises used: PNat.mod_add_div
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
⊢ (↑(m.mod k) : ℕ) + (↑k : ℕ) * m.div k = (↑m : ℕ)

Tactic:
exact mod_add_div _ _

Premises used: PNat.mod_add_div
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
rw : (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ) = (↑m : ℕ)
⊢ m.div k * (↑k : ℕ) + (↑(m.mod k) : ℕ) = (↑m : ℕ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
⊢ (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ) = (↑m : ℕ)

Tactic:
div_add_mod _ _

Premises used: PNat.div_add_mod
-- Module: Mathlib.Data.PNat.Basic
Goal:
m k : ℕ+
⊢ (↑k : ℕ) * m.div k + (↑(m.mod k) : ℕ) = (↑m : ℕ)

Tactic:
exact div_add_mod _ _

Premises used: PNat.div_add_mod