awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
norm_cast : multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k) + multiplicity p k - multiplicity p k
⊢ (↑(multiplicity p ((p ^ n).choose k)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(multiplicity p ((p ^ n).choose k)) : ℕ∞) (↑(multiplicity p k) : ℕ∞) -
      (↑(multiplicity p k) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
rw rw₁ : multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k)
⊢ multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k) + multiplicity p k - multiplicity p k

Tactic:
rw [Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
inl : ∀ (hkp : p ^ n < k), p ∣ (p ^ n).choose k
inr : ∀ (hkp : k < p ^ n), p ∣ (p ^ n).choose k
⊢ p ∣ (p ^ n).choose k

Tactic:
obtain hkp | hkp := hkp.symm.lt_or_gt

Premises used: Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

Tactic:
simp [choose_eq_zero_of_lt hkp]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
emultiplicity_ne_zero.1 fun h => hkp.not_ge <| Nat.le_of_dvd hk.bot_lt ?_

Premises used: Iff.mp, emultiplicity_ne_zero, LT.lt.not_ge, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
inr : ∀ (h : emultiplicity p ((p ^ n).choose k) = 0), p ^ n ∣ k
⊢ p ∣ (p ^ n).choose k

Tactic:
refine emultiplicity_ne_zero.1 fun h => hkp.not_ge <| Nat.le_of_dvd hk.bot_lt ?_

Premises used: Iff.mp, emultiplicity_ne_zero, LT.lt.not_ge, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k = (↑n : ℕ∞)

Tactic:
have H := hp.emultiplicity_choose_prime_pow_add_emultiplicity hkp.le hk
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : emultiplicity p ((p ^ n).choose k) + emultiplicity p k = (↑n : ℕ∞)
⊢ p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k

Tactic:
rw [h, zero_add, emultiplicity_eq_coe] at H

Premises used: zero_add, emultiplicity_eq_coe
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k

Tactic:
H.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp_1 : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k

Tactic:
exact H.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩

Premises used: Nat.Prime.dvd_choose_pow, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n k : ℕ
hp : Prime p
refine_1 : ∀ (h : p ∣ (p ^ n).choose k), k ≠ 0
refine_2 : ∀ (h : p ∣ (p ^ n).choose k), k ≠ p ^ n
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose 0
⊢ False

Tactic:
simp [hp.ne_one] at h

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose (p ^ n)
⊢ False

Tactic:
simp [hp.ne_one] at h

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
⊢ _root_.Prime (M := ℕ) 2

Tactic:
have h2 := prime_two.prime
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)

Tactic:
binaryRec ?_ ?_

Premises used: Nat.binaryRec
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
refine_1 : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
refine_2 :
  ∀ (b : Bool) (n : ℕ),
    (n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)

Tactic:
refine binaryRec ?_ ?_
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
⊢ Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)

Tactic:
fun h => False.elim <| h rfl

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
⊢ Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)

Tactic:
exact fun h => False.elim <| h rfl

Premises used: False.elim
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
pos : ∀ (hn : n = 0), emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)
neg : ∀ (hn : ¬n = 0), emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)
⊢ emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : n = 0
pos :
  ∀ (ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)) (h : bit b 0 ≠ 0),
    emultiplicity 2 (bit b 0)! < (↑(bit b 0) : ℕ∞)
⊢ emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)

Tactic:
subst hn
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : bit b 0 ≠ 0
⊢ b = true

Tactic:
simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h

Premises used: Bool.not_eq_false, Nat.bit_eq_zero_iff, ne_eq, true_and
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : b = true
pos : emultiplicity (α := ℕ) 2 1 < (↑1 : ℕ∞)
⊢ emultiplicity 2 (bit b 0)! < (↑(bit b 0) : ℕ∞)

Tactic:
simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]

Premises used: Nat.bit, cond_true, zero_add, MulZeroClass.mul_zero, Nat.factorial_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : b = true
pos : LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)
pos₁ : Prime 2
⊢ emultiplicity (α := ℕ) 2 1 < (↑1 : ℕ∞)

Tactic:
rw [Prime.emultiplicity_one]

Premises used: Nat.Prime.emultiplicity_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : b = true
⊢ LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)

Tactic:
zero_lt_one

Premises used: WithTop.some, zero_lt_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : b = true
⊢ LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
ih : Ne (α := ℕ) 0 0 → emultiplicity 2 0! < (↑0 : ℕ∞)
h : b = true
⊢ Prime 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
rw : emultiplicity 2 n ! + (↑n : ℕ∞) < (↑(2 * n) : ℕ∞)
⊢ emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)

Tactic:
rw [prime_two.emultiplicity_factorial_mul]

Premises used: Nat.Prime.emultiplicity_factorial_mul, Nat.prime_two
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
rw : emultiplicity 2 n ! + (↑n : ℕ∞) < (↑(n + n) : ℕ∞)
⊢ emultiplicity 2 n ! + (↑n : ℕ∞) < (↑(2 * n) : ℕ∞)

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
apply : Ne (α := WithTop ℕ) (↑n : ℕ∞) ⊤
⊢ emultiplicity 2 n ! + (↑n : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)

Tactic:
apply WithTop.add_lt_add_right _ (ih hn)

Premises used: WithTop.add_lt_add_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
⊢ Ne (α := WithTop ℕ) (↑n : ℕ∞) ⊤

Tactic:
Ne.symm nofun

Premises used: False, Ne.symm, _private.0.Nat.emultiplicity_two_factorial_lt.match_1
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
⊢ Ne (α := WithTop ℕ) (↑n : ℕ∞) ⊤

Tactic:
exact Ne.symm nofun

Premises used: False, Ne.symm, _private.0.match_1
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)

Tactic:
have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by
      rw [prime_two.emultiplicity_factorial_mul]
      rw [two_mul]
      push_cast
      apply WithTop.add_lt_add_right _ (ih hn)
      exact Ne.symm nofun
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
h : bit b n ≠ 0
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
neg : ∀ (h : bit false n ≠ 0), emultiplicity 2 (bit false n)! < (↑(bit false n) : ℕ∞)
neg₁ : ∀ (h : bit true n ≠ 0), emultiplicity 2 (bit true n)! < (↑(bit true n) : ℕ∞)
⊢ emultiplicity 2 (bit b n)! < (↑(bit b n) : ℕ∞)

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < (↑(bit false n) : ℕ∞)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this_1 : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
this : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1
⊢ emultiplicity 2 (bit true n)! < (↑(bit true n) : ℕ∞)

Tactic:
simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Premises used: Nat.bit, Nat.prime_two, Nat.factorial, emultiplicity_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
neg : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1
⊢ emultiplicity 2 (bit true n)! < (↑(bit true n) : ℕ∞)

Tactic:
suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
neg : emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1
⊢ emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1

Tactic:
rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]

Premises used: Iff.mpr, Nat.two_not_dvd_two_mul_add_one, emultiplicity_eq_zero, zero_add
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1

Tactic:
this.trans ?_

Premises used: LT.lt.trans
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
neg : (↑(2 * n) : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1
⊢ emultiplicity 2 (2 * n)! < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1

Tactic:
refine this.trans ?_

Premises used: LT.lt.trans
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
⊢ (↑(2 * n) : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1

Tactic:
mod_cast lt_succ_self _

Premises used: HMul.hMul, congrArg, Nat.cast_lt._simp_1, Nat.cast_add._simp_1, cast, Nat.lt_succ_self, Nat.cast, HAdd.hAdd, LT.lt, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
h2 : _root_.Prime (M := ℕ) 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < (↑n : ℕ∞)
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < (↑(2 * n) : ℕ∞)
h : bit true n ≠ 0
⊢ (↑(2 * n) : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑(2 * n) : ℕ∞) 1

Tactic:
exact mod_cast lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Data.Nat.Nth
Goal:
p_1 p : ℕ → Prop
n : ℕ
⊢ ℕ

Tactic:
exact
    if h : Set.Finite (setOf p) then h.toFinset.sort.getD n 0
    else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n

Premises used: setOf, Set.Finite
-- Module: Mathlib.Data.Nat.Nth
Goal:
p_1 p : ℕ → Prop
n : ℕ
⊢ ℕ

Tactic:
classical exact
    if h : Set.Finite (setOf p) then h.toFinset.sort.getD n 0
    else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n

Premises used: setOf, Set.Finite
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : #(hf.toFinset (s := setOf p)) ≤ n
hn₁ : (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length ≤ n
⊢ nth p n = 0

Tactic:
rw [nth, dif_pos hf, List.getD_eq_default]

Premises used: dif_pos, List.getD_eq_default, Nat.nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn hn₁ hn₂ hn₃ hn₄ : #(hf.toFinset (s := setOf p)) ≤ n
⊢ (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length ≤ n

Tactic:
rwa [Finset.length_sort]

Premises used: Finset.length_sort
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h : (setOf p).Finite
n : ℕ
⊢ nth p n = (h.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).getD n 0

Tactic:
dif_pos h

Premises used: dif_pos, Nat.nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
rw :
  (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).getD n 0 =
    (hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
      (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p)))
rw₁ :
  (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).getD n 0 =
    getElem (valid := fun (xs : List ℕ) (i : Fin #(hf.toFinset (s := setOf p))) ↦ (↑i : ℕ) < xs.length)
      (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b) (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) ⋯
rw₂ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b) n
      ⋯ =
    getElem (valid := fun (xs : List ℕ) (i : Fin #(hf.toFinset (s := setOf p))) ↦ (↑i : ℕ) < xs.length)
      (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b) (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) ⋯
hn₁ : n < (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length
rw₃ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b) n
      ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b)
      (↑(⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) : ℕ) ⋯
hn₂ : n < (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length
rw₄ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b) n
      ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b)
      (↑(⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) : ℕ) ⋯
hn₃ : n < (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length
⊢ nth p n =
    (hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
      (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p)))

Tactic:
rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_getElem, Fin.getElem_fin]

Premises used: List.getD_eq_getElem, Finset.orderEmbOfFin_apply, Fin.getElem_fin, Nat.nth_eq_getD_sort
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #(hf.toFinset (s := setOf p))
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : m < n
simp :
  LT.lt (α := ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨m, hm⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)
⊢ nth p m < nth p n

Tactic:
simp only [nth_eq_orderEmbOfFin, *]

Premises used: Nat.nth_eq_orderEmbOfFin
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #(hf.toFinset (s := setOf p))
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : m < n
⊢ LT.lt (α := ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨m, hm⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)

Tactic:
OrderEmbedding.strictMono _ h

Premises used: OrderEmbedding.strictMono
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m : ℕ
hm : m < #(hf.toFinset (s := setOf p))
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : m < n
⊢ LT.lt (α := ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨m, hm⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)
    ((hf.toFinset (s := setOf p).orderEmbOfFin ⋯ : (a : Fin #hf.toFinset) → ℕ)
        (⟨n, hn⟩ : Fin #(hf.toFinset (s := setOf p))) :
      ℕ)

Tactic:
exact OrderEmbedding.strictMono _ h

Premises used: OrderEmbedding.strictMono
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m n : ℕ
h : m < n
hn : n < #(hf.toFinset (s := setOf p))
⊢ nth p m < nth p n

Tactic:
nth_strictMonoOn hf (h.trans hn) hn h

Premises used: Nat.nth_strictMonoOn, LT.lt.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m n : ℕ
h : m ≤ n
hn : n < #(hf.toFinset (s := setOf p))
⊢ nth p m ≤ nth p n

Tactic:
(nth_strictMonoOn hf).monotoneOn (h.trans_lt hn) hn h

Premises used: StrictMonoOn.monotoneOn, Nat.nth_strictMonoOn, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m n : ℕ
h : nth p m < nth p n
hm : m < #(hf.toFinset (s := setOf p))
⊢ m < n

Tactic:
not_le.1 fun hle => h.not_ge <| nth_le_nth_of_lt_card hf hle hm

Premises used: not_le, Nat.nth_le_nth_of_lt_card, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
m n : ℕ
h : nth p m ≤ nth p n
hm : m < #(hf.toFinset (s := setOf p))
⊢ m ≤ n

Tactic:
not_lt.1 fun hlt => h.not_gt <| nth_lt_nth_of_lt_card hf hlt hm

Premises used: not_lt, LE.le.not_gt, Iff.mp, Nat.nth_lt_nth_of_lt_card
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
⊢ Set.InjOn (nth p) (Set.Iio #(hf.toFinset (s := setOf p)))

Tactic:
(nth_strictMonoOn hf).injOn

Premises used: StrictMonoOn.injOn, Nat.nth_strictMonoOn
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
⊢ Set.range (nth p) = insert 0 (setOf p)

Tactic:
simpa only [← List.getD_eq_getElem?_getD, ← nth_eq_getD_sort hf, mem_sort,
    Set.Finite.mem_toFinset] using Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0

Premises used: Finset.mem_sort, Set.Finite.mem_toFinset, LE.le, Set.Finite.toFinset, Set.range_list_getD, Nat.nth_eq_getD_sort, Finset.sort, OfNat.ofNat, List.getD_eq_getElem?_getD
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
h :
  ∀ (x : ℕ),
    x ∈ nth p '' Set.Iio #(hf.toFinset (s := setOf p)) ↔
      Membership.mem (γ := Set ℕ)
        (Set.range (ι := Fin #(hf.toFinset (s := setOf p)))
          (⇑(hf.toFinset (s := setOf p).orderEmbOfFin ⋯) : (a : Fin #hf.toFinset) → ℕ))
        x
⊢ nth p '' Set.Iio #(hf.toFinset (s := setOf p)) =
    Set.range (ι := Fin #(hf.toFinset (s := setOf p)))
      (⇑(hf.toFinset (s := setOf p).orderEmbOfFin ⋯) : (a : Fin #hf.toFinset) → ℕ)

Tactic:
ext x
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
x : ℕ
⊢ x ∈ nth p '' Set.Iio #(hf.toFinset (s := setOf p)) ↔
    Membership.mem (γ := Set ℕ)
      (Set.range (ι := Fin #(hf.toFinset (s := setOf p)))
        (⇑(hf.toFinset (s := setOf p).orderEmbOfFin ⋯) : (a : Fin #hf.toFinset) → ℕ))
      x

Tactic:
simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
        Set.mem_Iio, exists_prop]

Premises used: Set.mem_range, Set.mem_Iio, Set.mem_image, exists_prop, Nat.nth_eq_orderEmbOfFin, Fin.exists_iff
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
rw : (↑(hf.toFinset (s := setOf p)) : Set ℕ) = setOf p
rw₁ rw₂ : setOf p = setOf p
⊢ Set.range (ι := Fin #(hf.toFinset (s := setOf p)))
      (⇑(hf.toFinset (s := setOf p).orderEmbOfFin ⋯) : (a : Fin #hf.toFinset) → ℕ) =
    setOf p

Tactic:
rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, Finset.range_orderEmbOfFin
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hlt : n < #(hf.toFinset (s := setOf p))
⊢ p (nth p n)

Tactic:
(image_nth_Iio_card hf).subset <| Set.mem_image_of_mem _ hlt

Premises used: Set.Mem, setOf, Eq.subset, Set.mem_image_of_mem, Nat.image_nth_Iio_card
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Finite
x : ℕ
h : p x
rwa : ∀ (h : Membership.mem (γ := Set ℕ) {y : ℕ | p y} x), ∃ n < #(hf.toFinset (s := setOf p)), nth p n = x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : x ∈ nth p '' Set.Iio #(hf.toFinset (s := setOf p))), ∃ n < #(hf.toFinset (s := setOf p)), nth p n = x
⊢ ∃ n < #(hf.toFinset (s := setOf p)), nth p n = x

Tactic:
rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h

Premises used: Set.mem_setOf_eq, Nat.image_nth_Iio_card
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
n : ℕ
rw :
  Eq (α := ℕ)
    (if h : (setOf p).Finite then (h.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).getD n 0
    else (↑((Subtype.orderIsoOfNat (setOf p) : (a : ℕ) → (↑(setOf p) : Type)) n) : ℕ))
    (↑((Subtype.orderIsoOfNat (setOf p) : (a : ℕ) → (↑(setOf p) : Type)) n) : ℕ)
rw₁ rw₂ :
  Eq (α := ℕ) (↑((Subtype.orderIsoOfNat (setOf p) : (a : ℕ) → (↑(setOf p) : Type)) n) : ℕ)
    (↑((Subtype.orderIsoOfNat (setOf p) : (a : ℕ) → (↑(setOf p) : Type)) n) : ℕ)
⊢ nth p n = (↑((Subtype.orderIsoOfNat (setOf p) : (a : ℕ) → (↑(setOf p) : Type)) n) : ℕ)

Tactic:
rw [nth, dif_neg hf]

Premises used: dif_neg, Nat.nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ nth p =
    Function.comp (β := (↑(setOf p) : Type)) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ setOf p))
      (⇑(Subtype.orderIsoOfNat (setOf p)) : (a : ℕ) → (↑(setOf p) : Type))

Tactic:
funext <| nth_apply_eq_orderIsoOfNat hf

Premises used: funext, Nat.nth_apply_eq_orderIsoOfNat
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
rw :
  StrictMono (α := ℕ) (β := ℕ)
    (Function.comp (β := (↑(setOf p) : Type)) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ setOf p))
      (⇑(Subtype.orderIsoOfNat (setOf p)) : (a : ℕ) → (↑(setOf p) : Type)))
⊢ StrictMono (nth p)

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Premises used: Nat.nth_eq_orderIsoOfNat