awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ StrictMono (α := ℕ) (β := ℕ)
    (Function.comp (β := (↑(setOf p) : Type)) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ setOf p))
      (⇑(Subtype.orderIsoOfNat (setOf p)) : (a : ℕ) → (↑(setOf p) : Type)))

Tactic:
(Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

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

Tactic:
exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

Premises used: OrderIso.strictMono, StrictMono.comp, Subtype.strictMono_coe
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Function.Injective (nth p)

Tactic:
(nth_strictMono hf).injective

Premises used: Nat.nth_strictMono, StrictMono.injective
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Monotone (nth p)

Tactic:
(nth_strictMono hf).monotone

Premises used: Nat.nth_strictMono, StrictMono.monotone
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
k n : ℕ
⊢ nth p k < nth p n ↔ k < n

Tactic:
(nth_strictMono hf).lt_iff_lt

Premises used: Nat.nth_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
k n : ℕ
⊢ nth p k ≤ nth p n ↔ k ≤ n

Tactic:
(nth_strictMono hf).le_iff_le

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

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Premises used: Nat.nth_eq_orderIsoOfNat
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Infinite (↑(setOf p) : Type)

Tactic:
haveI := hf.to_subtype
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
this : Infinite (↑(setOf p) : Type)
⊢ Set.range (ι := ℕ)
      (Function.comp (β := (↑(setOf p) : Type)) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ setOf p))
        (⇑(Subtype.orderIsoOfNat (setOf p)) : (a : ℕ) → (↑(setOf p) : Type))) =
    setOf p

Tactic:
Nat.Subtype.coe_comp_ofNat_range

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

Tactic:
exact Nat.Subtype.coe_comp_ofNat_range

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

Tactic:
classical exact Nat.Subtype.coe_comp_ofNat_range

Premises used: Nat.Subtype.coe_comp_ofNat_range
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
n : ℕ
⊢ p (nth p n)

Tactic:
Set.range_subset_iff.1 (range_nth_of_infinite hf).le n

Premises used: Set.Mem, setOf, Eq.le, Iff.mp, Nat.range_nth_of_infinite, Set.range_subset_iff
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
(setOf p).finite_or_infinite.elim (fun hf => ?_) fun hf => ?_

Premises used: Set.finite_or_infinite, setOf, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
refine_1 :
  ∀ (hf : (setOf p).Finite), ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
refine_2 :
  ∀ (hf : (setOf p).Infinite), ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
refine (setOf p).finite_or_infinite.elim (fun hf => ?_) fun hf => ?_

Premises used: Set.finite_or_infinite, setOf, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
refine_1 :
  ∀ (n : ℕ) (hn : n < #(hf.toFinset (s := setOf p))) (hx : nth p n = x),
    ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩

Premises used: Nat.exists_lt_card_finite_nth_eq
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
hx : nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
⟨n, fun _ => hn, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
hx : nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
exact ⟨n, fun _ => hn, hx⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Infinite
⊢ x ∈ Set.range (nth p)

Tactic:
rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h

Premises used: Set.mem_setOf_eq, Nat.range_nth_of_infinite
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Infinite
h₁ : x ∈ Set.range (nth p)
⊢ (setOf p).Infinite

Tactic:
rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h

Premises used: Set.mem_setOf_eq, Nat.range_nth_of_infinite
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : (setOf p).Infinite
refine_2 :
  ∀ (n : ℕ) (hx : nth p n = x), ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
rcases h with ⟨n, hx⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
hf : (setOf p).Infinite
n : ℕ
hx : nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
⟨n, fun hf' => absurd hf' hf, hx⟩

Premises used: absurd, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
x : ℕ
hf : (setOf p).Infinite
n : ℕ
hx : nth p n = x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x

Tactic:
exact ⟨n, fun hf' => absurd hf' hf, hx⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
⊢ setOf p ⊆ Set.range (nth p)

Tactic:
fun x (hx : p x) =>
  let ⟨n, _, hn⟩ := exists_lt_card_nth_eq hx
  ⟨n, hn⟩

Premises used: Set.Mem, setOf, Membership.mem, _private.0.Nat.subset_range_nth.match_1, Set.Subset, Nat.exists_lt_card_nth_eq, Exists.intro, Nat.nth, Set.range
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
⊢ Set.range (nth p) ⊆ insert 0 (setOf p)

Tactic:
(setOf p).finite_or_infinite.elim (fun h => (range_nth_of_finite h).subset) fun h =>
    (range_nth_of_infinite h).trans_subset (Set.subset_insert _ _)

Premises used: Set.finite_or_infinite, setOf, Eq.subset, Nat.range_nth_of_finite, Nat.range_nth_of_infinite, Or.elim, OfNat.ofNat, Set.subset_insert, Eq.trans_subset
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ p (nth p n)

Tactic:
(setOf p).finite_or_infinite.elim (fun hf => nth_mem_of_lt_card hf (h hf)) fun h =>
    nth_mem_of_infinite h n

Premises used: Set.finite_or_infinite, setOf, Nat.nth_mem_of_lt_card, Nat.nth_mem_of_infinite, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
hlt : m < n
h : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p m < nth p n

Tactic:
(setOf p).finite_or_infinite.elim (fun hf => nth_lt_nth_of_lt_card hf hlt (h _)) fun hf =>
    (nth_lt_nth hf).2 hlt

Premises used: Iff.mpr, Set.finite_or_infinite, setOf, Nat.nth_lt_nth, Nat.nth_lt_nth_of_lt_card, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
hle : m ≤ n
h : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p m ≤ nth p n

Tactic:
(setOf p).finite_or_infinite.elim (fun hf => nth_le_nth_of_lt_card hf hle (h _)) fun hf =>
    (nth_le_nth hf).2 hle

Premises used: Iff.mpr, Set.finite_or_infinite, setOf, Nat.nth_le_nth_of_lt_card, Nat.nth_le_nth, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ n ≤ nth p n

Tactic:
(setOf p).finite_or_infinite.elim
    (fun hf => ((nth_strictMonoOn hf).mono <| Set.Iic_subset_Iio.2 (h _)).Iic_id_le _ le_rfl)
    fun hf => (nth_strictMono hf).id_le _

Premises used: Iff.mpr, StrictMonoOn.Iic_id_le, le_rfl, Nat.nth_strictMono, Set.finite_or_infinite, setOf, StrictMonoOn.mono, Set.Iic_subset_Iio, Nat.nth_strictMonoOn, StrictMono.id_le, Or.elim
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ IsLeast {i : ℕ | p i ∧ ∀ k < n, nth p k < i} (nth p n)

Tactic:
⟨⟨nth_mem n h, fun _k hk => nth_lt_nth' hk h⟩, fun _x hx =>
    let ⟨k, hk, hkx⟩ := exists_lt_card_nth_eq hx.1
    (lt_or_ge k n).elim (fun hlt => absurd hkx (hx.2 _ hlt).ne) fun hle => hkx ▸ nth_le_nth' hle hk⟩

Premises used: Nat.nth_mem, _private.0.Nat.subset_range_nth.match_1, Eq.rec, Nat.nth_le_nth', LE.le, IsLeast, Nat.nth_lt_nth', Nat.exists_lt_card_nth_eq, absurd, And.right, And.left, And.intro, lt_or_ge, Nat.nth, Or.elim, LT.lt.ne
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : n < #(hf.toFinset (s := setOf p))
⊢ IsLeast {i : ℕ | p i ∧ ∀ k < n, nth p k < i} (nth p n)

Tactic:
isLeast_nth fun _ => hn

Premises used: Nat.isLeast_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
hf : (setOf p).Infinite
n : ℕ
⊢ IsLeast {i : ℕ | p i ∧ ∀ k < n, nth p k < i} (nth p n)

Tactic:
isLeast_nth fun h => absurd h hf

Premises used: Nat.isLeast_nth, absurd
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
pos :
  ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))),
    nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
neg :
  ∀ (hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n),
    nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}

Tactic:
by_cases! hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}

Tactic:
(isLeast_nth hn).csInf_eq.symm

Premises used: IsLeast.csInf_eq, Nat.isLeast_nth, Eq.symm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}

Tactic:
exact (isLeast_nth hn).csInf_eq.symm

Premises used: IsLeast.csInf_eq, Nat.isLeast_nth, Eq.symm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
⊢ (setOf p).Finite

Tactic:
rcases hn with ⟨hf, hn⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
hf : (setOf p).Finite
⊢ #(⋯.toFinset (s := setOf p)) ≤ n

Tactic:
rcases hn with ⟨hf, hn⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
neg : Eq (α := ℕ) 0 (sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x})
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}

Tactic:
rw [nth_of_card_le _ hn]

Premises used: Nat.nth_of_card_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
⊢ Eq (α := ℕ) 0 (sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x})

Tactic:
((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm

Premises used: congr_arg, Set.eq_empty_of_forall_notMem, Nat.sInf_empty, Eq.symm, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
neg : ∀ (k : ℕ) (hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} k), False
⊢ Eq (α := ℕ) 0 (sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x})

Tactic:
refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm

Premises used: congr_arg, Set.eq_empty_of_forall_notMem, Nat.sInf_empty, Eq.symm, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
k : ℕ
hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} k
neg :
  ∀ (k : ℕ) (hlt : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p)))
    (hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} (nth p k)), False
⊢ False

Tactic:
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩

Premises used: Nat.exists_lt_card_nth_eq, And.left, rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))
hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} (nth p k)
⊢ False

Tactic:
(hk.2 _ ((hlt hf).trans_le hn)).false

Premises used: And.right, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))
hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} (nth p k)
⊢ False

Tactic:
exact (hk.2 _ ((hlt hf).trans_le hn)).false

Premises used: And.right, LT.lt.trans_le, LT.lt.false
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
rw : sInf {x : ℕ | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)
⊢ nth p 0 = sInf (setOf p)

Tactic:
rw [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
⊢ sInf {x : ℕ | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0

Tactic:
simp [nth_zero, h]

Premises used: Nat.nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
rw : sInf (setOf p) = Nat.find (p := p) h
⊢ nth p 0 = Nat.find (p := p) h

Tactic:
rw [nth_zero]

Premises used: Nat.nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ sInf p = Nat.find (p := fun (n : ℕ) ↦ n ∈ p) h

Tactic:
Nat.sInf_def h

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ sInf (setOf p) = Nat.find (p := p) h

Tactic:
convert! Nat.sInf_def h

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
hf : (setOf p).Finite
⊢ ¬(p 0 ∧ n = 0) ∧ ∀ (x : (setOf p).Finite), n < #(x.toFinset (s := setOf p))

Tactic:
simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h

Premises used: not_le, Nat.nth_eq_zero, not_exists, ne_eq, not_or
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
h : ¬(p 0 ∧ n = 0) ∧ ∀ (x : (setOf p).Finite), n < #(x.toFinset (s := setOf p))
⊢ n < #(hf.toFinset (s := setOf p))

Tactic:
h.2 hf

Premises used: And.right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
h : ¬(p 0 ∧ n = 0) ∧ ∀ (x : (setOf p).Finite), n < #(x.toFinset (s := setOf p))
⊢ n < #(hf.toFinset (s := setOf p))

Tactic:
exact h.2 hf

Premises used: And.right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
⊢ p (nth p n)

Tactic:
nth_mem n (lt_card_toFinset_of_nth_ne_zero h)

Premises used: Nat.nth_mem, Nat.lt_card_toFinset_of_nth_ne_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
simp :
  ∀ (ha : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ a),
    ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
⊢ nth p b = 0

Tactic:
simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢

Premises used: Nat.nth_eq_zero, false_and, false_or
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ a
⊢ ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b

Tactic:
ha.imp fun hf hle => hle.trans hab

Premises used: Exists.imp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ a
⊢ ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b

Tactic:
exact ha.imp fun hf hle => hle.trans hab

Premises used: Exists.imp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
hb : nth p b ≠ 0
⊢ nth p a ≠ 0

Tactic:
mt (nth_eq_zero_mono h₀ hab) hb

Premises used: mt, Nat.nth_eq_zero_mono
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
inl : ∀ (hf : (setOf p).Finite), a ≤ nth p k
inr : ∀ (hf : (setOf p).Infinite), a ≤ nth p k
⊢ a ≤ nth p k

Tactic:
rcases (setOf p).finite_or_infinite with hf | hf

Premises used: Set.finite_or_infinite, setOf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Finite
inl :
  ∀ (n : ℕ) (hn : n < #(hf.toFinset (s := setOf p))) (h : nth p n < nth p (k + 1)) (ha : p (nth p n)), nth p n ≤ nth p k
⊢ a ≤ nth p k

Tactic:
rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩

Premises used: Nat.exists_lt_card_finite_nth_eq, rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < nth p (k + 1)
ha : p (nth p n)
inl : ∀ (hk : k + 1 < #(hf.toFinset (s := setOf p))), nth p n ≤ nth p k
inl₁ : ∀ (hk : #(hf.toFinset (s := setOf p)) ≤ k + 1), nth p n ≤ nth p k
⊢ nth p n ≤ nth p k

Tactic:
rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk

Premises used: HAdd.hAdd, Set.Finite.toFinset, Finset.card, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #(hf.toFinset (s := setOf p))
inl : ∀ (h : n < k + 1) (ha : p (nth p n)) (hk : k + 1 < #(hf.toFinset (s := setOf p))), nth p n ≤ nth p k
inl₁ : ∀ (h : n ≤ k) (ha : p (nth p n)) (hk : k + 1 < #(hf.toFinset (s := setOf p))), nth p n ≤ nth p k
inl₂ inl₃ inl₄ inl₅ :
  ∀ (h : nth p n ≤ nth p k) (ha : p (nth p n)) (hk : k + 1 < #(hf.toFinset (s := setOf p))), nth p n ≤ nth p k
⊢ nth p n ≤ nth p k

Tactic:
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
        ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h

Premises used: Nat.lt_succ_self, Nat.lt_succ_iff, Nat.nth_strictMonoOn, LT.lt.trans, StrictMonoOn.le_iff_le, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #(hf.toFinset (s := setOf p)) ≤ k + 1
⊢ nth p n < 0

Tactic:
rw [nth_of_card_le _ hk] at h

Premises used: Nat.nth_of_card_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #(hf.toFinset (s := setOf p)) ≤ k + 1
h₁ : nth p n < 0
⊢ p (nth p n)

Tactic:
rw [nth_of_card_le _ hk] at h

Premises used: Nat.nth_of_card_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #(hf.toFinset (s := setOf p)) ≤ k + 1
h₁ : nth p n < 0
ha₁ : p (nth p n)
⊢ #(hf.toFinset (s := setOf p)) ≤ k + 1

Tactic:
rw [nth_of_card_le _ hk] at h

Premises used: Nat.nth_of_card_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < 0
ha : p (nth p n)
hk : #(hf.toFinset (s := setOf p)) ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
absurd h (zero_le _).not_gt

Premises used: Nat.zero_le, absurd, LE.le.not_gt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #(hf.toFinset (s := setOf p))
h : nth p n < 0
ha : p (nth p n)
hk : #(hf.toFinset (s := setOf p)) ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
exact absurd h (zero_le _).not_gt

Premises used: Nat.zero_le, absurd, LE.le.not_gt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Infinite
inr : ∀ (n : ℕ) (h : nth p n < nth p (k + 1)) (ha : p (nth p n)), nth p n ≤ nth p k
⊢ a ≤ nth p k

Tactic:
rcases subset_range_nth ha with ⟨n, rfl⟩

Premises used: rfl, Nat.subset_range_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
inr : ∀ (h : n < k + 1) (ha : p (nth p n)), nth p n ≤ nth p k
inr₁ : ∀ (h : n ≤ k) (ha : p (nth p n)), nth p n ≤ nth p k
inr₂ inr₃ inr₄ inr₅ : ∀ (h : nth p n ≤ nth p k) (ha : p (nth p n)), nth p n ≤ nth p k
⊢ nth p n ≤ nth p k

Tactic:
rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

Premises used: Nat.nth_lt_nth, Nat.lt_succ_iff, Nat.nth_le_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
pos : ∀ (h' : ∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))), p (nth p a)
neg : ∀ (h' : ¬∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))), p (nth p a)
⊢ p (nth p a)

Tactic:
by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))
⊢ p (nth p a)

Tactic:
nth_mem a h'

Premises used: Nat.nth_mem
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))
⊢ p (nth p a)

Tactic:
exact nth_mem a h'

Premises used: Nat.nth_mem
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))
⊢ ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a

Tactic:
simp only [not_forall, not_lt] at h'

Premises used: not_lt, Classical.not_forall
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
⊢ (setOf p).Finite

Tactic:
rcases h' with ⟨hf, ha⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
hf : (setOf p).Finite
⊢ #(⋯.toFinset (s := setOf p)) ≤ a

Tactic:
rcases h' with ⟨hf, ha⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
hf : (setOf p).Finite
ha : #(⋯.toFinset (s := setOf p)) ≤ a
⊢ ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b

Tactic:
⟨hf, ha.trans hab⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
hf : (setOf p).Finite
ha : #(⋯.toFinset (s := setOf p)) ≤ a
⊢ ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b

Tactic:
exact ⟨hf, ha.trans hab⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
neg : ∀ (h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b), p (nth p a)
⊢ p (nth p a)

Tactic:
have h'b : ∃ hf : (setOf p).Finite, #hf.toFinset ≤ b := by
      rcases h' with ⟨hf, ha⟩
      exact ⟨hf, ha.trans hab⟩