awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
h₁ : ∀ (he : i ∈ setOf p'), i ∈ f '' {i : ℕ | p' (f i)}
⊢ i ∈ f '' {i : ℕ | p' (f i)} ↔ i ∈ setOf p'

Tactic:
refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
he : i ∈ setOf p'
h₁ : ∀ (t : ℕ) (he : f t ∈ setOf p'), f t ∈ f '' {i : ℕ | p' (f i)}
⊢ i ∈ f '' {i : ℕ | p' (f i)}

Tactic:
rcases h0p' _ he with ⟨t, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
t : ℕ
he : f t ∈ setOf p'
⊢ f t ∈ f '' {i : ℕ | p' (f i)}

Tactic:
⟨t, he, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
t : ℕ
he : f t ∈ setOf p'
⊢ f t ∈ f '' {i : ℕ | p' (f i)}

Tactic:
exact ⟨t, he, rfl⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
⊢ ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'

Tactic:
have hs {p' : ℕ → Prop} (h0p' : ∀ k, p' k → k ∈ Set.range f) :
      f '' {i | p' (f i)} = setOf p' := by
    ext i
    refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
    rcases h0p' _ he with ⟨t, rfl⟩
    exact ⟨t, he, rfl⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #(hfi.toFinset (s := setOf p))
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
induction :
  ∀ (h : ∀ (hfi : (setOf p).Finite), 0 < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) 0) = nth p 0
hi :
  ∀ (n : ℕ),
    (∀ m ≤ n,
        ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))),
          f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m) →
      ∀ (h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))),
        f (nth (fun (i : ℕ) ↦ p (f i)) (n + 1)) = nth p (n + 1)
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) n) = nth p n

Tactic:
induction n using Nat.case_strong_induction_on

Premises used: Nat.case_strong_induction_on
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #(hfi.toFinset (s := setOf p))
simp_rw : f (sInf {i : ℕ | p (f i)}) = sInf (setOf p)
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) 0) = nth p 0

Tactic:
simp_rw [nth_zero]

Premises used: Nat.nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #(hfi.toFinset (s := setOf p))
⊢ p (nth p 0)

Tactic:
replace h := nth_mem _ h
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : p (nth p 0)
rw : Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}
⊢ f (sInf {i : ℕ | p (f i)}) = sInf (setOf p)

Tactic:
rw [← hs h0, ← hf.monotone.map_csInf]

Premises used: StrictMono.monotone, Monotone.map_csInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : p (nth p 0)
rcases : ∀ (t : ℕ) (ht : f t = nth p 0), Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}

Tactic:
rcases h0 _ h with ⟨t, ht⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : p (nth p 0)
t : ℕ
ht : f t = nth p 0
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}

Tactic:
⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩

Premises used: Eq.rec, Set.mem_setOf_eq, Set.Nonempty, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : p (nth p 0)
t : ℕ
ht : f t = nth p 0
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}

Tactic:
exact ⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #(hfi.toFinset (s := setOf p))
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) 0) = nth p 0

Tactic:
case _ =>
    simp_rw [nth_zero]
    replace h := nth_mem _ h
    rw [← hs h0, ← hf.monotone.map_csInf]
    rcases h0 _ h with ⟨t, ht⟩
    exact ⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩

Premises used: StrictMono.monotone, Nat.nth_zero, Monotone.map_csInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
nth_rw : f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) = nth p (n + 1)
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) (n + 1)) = nth p (n + 1)

Tactic:
nth_rw 1 [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
nth_rw :
  f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
⊢ f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) = nth p (n + 1)

Tactic:
nth_rw 1 [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
repeat :
  f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) (n + 1)) = nth p (n + 1)

Tactic:
repeat nth_rw 1 [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
⊢ ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f

Tactic:
have h0' : ∀ k', (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f := fun _ h ↦ h0 _ h.1
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
rw :
  f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    f (sInf {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i})
rw₁ : Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}
⊢ f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}

Tactic:
rw [← hs h0', ← hf.monotone.map_csInf]

Premises used: StrictMono.monotone, Monotone.map_csInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x})

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
h₁ : ∀ (k m' : ℕ) (hm : m' < n + 1), nth p m' < f k ↔ nth (fun (i : ℕ) ↦ p (f i)) m' < k
⊢ f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) =
    f (sInf {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

Tactic:
convert! rfl using 8 with k m' hm

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
h₁ : nth p m' < f k ↔ f (nth (fun (i : ℕ) ↦ p (f i)) m') < f k
⊢ nth p m' < f k ↔ nth (fun (i : ℕ) ↦ p (f i)) m' < k

Tactic:
nth_rw 2 [← hf.lt_iff_lt]

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ nth p m' < f k ↔ nth p m' < f k

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
h₁ : f (nth (fun (i : ℕ) ↦ p (f i)) m') = nth p m'
⊢ nth p m' < f k ↔ f (nth (fun (i : ℕ) ↦ p (f i)) m') < f k

Tactic:
convert! Iff.rfl using 2

Premises used: Iff.rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) m') = nth p m'

Tactic:
ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)

Premises used: Nat.lt_add_one_iff, Iff.mp, LT.lt.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) m') = nth p m'

Tactic:
exact ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)

Premises used: Nat.lt_add_one_iff, Iff.mp, LT.lt.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
rcases : ∀ (t : ℕ) (ht : f t = nth p (n + 1)), Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}

Tactic:
rcases h0 _ (nth_mem _ h) with ⟨t, ht⟩

Premises used: Nat.nth_mem
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
t : ℕ
ht : f t = nth p (n + 1)
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}

Tactic:
⟨t, ht ▸ (nth_mem _ h), fun _ hk ↦ ht ▸ nth_lt_nth' hk h⟩

Premises used: Nat.nth_mem, Eq.rec, Nat.nth_lt_nth', Set.Nonempty, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop} (h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f), f '' {i : ℕ | p' (f i)} = setOf p'
n : ℕ
ih :
  ∀ m ≤ n,
    ∀ (h : ∀ (hfi : (setOf p).Finite), m < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #(hfi.toFinset (s := setOf p))
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
t : ℕ
ht : f t = nth p (n + 1)
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}

Tactic:
exact ⟨t, ht ▸ (nth_mem _ h), fun _ hk ↦ ht ▸ nth_lt_nth' hk h⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun (i : ℕ) ↦ p (i + m)) n + m = nth p n

Tactic:
nth_comp_of_strictMono (strictMono_id.add_const m) (fun k hk ↦ ?_)
    (fun hf ↦ lt_card_toFinset_of_nth_ne_zero h hf)

Premises used: Set.Mem, setOf, Nat.lt_card_toFinset_of_nth_ne_zero, dite, strictMono_id, StrictMono.add_const, Nat.nth, Nat.nth_comp_of_strictMono
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
refine : ∀ (k : ℕ) (hk : p k), Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ id x + m) k
⊢ nth (fun (i : ℕ) ↦ p (i + m)) n + m = nth p n

Tactic:
refine nth_comp_of_strictMono (strictMono_id.add_const m) (fun k hk ↦ ?_)
    (fun hf ↦ lt_card_toFinset_of_nth_ne_zero h hf)

Premises used: Nat.lt_card_toFinset_of_nth_ne_zero, strictMono_id, StrictMono.add_const, Nat.nth_comp_of_strictMono
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
by_contra : ∀ (hn : k ∉ Set.range fun (x : ℕ) ↦ id x + m), False
⊢ Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ id x + m) k

Tactic:
by_contra hn
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : k ∉ Set.range fun (x : ℕ) ↦ id x + m
⊢ ¬∃ (y : ℕ), k = y + m

Tactic:
simp_rw [id_eq, Set.mem_range, eq_comm] at hn

Premises used: Set.mem_range, eq_comm, id_eq
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ (y : ℕ), k = y + m
⊢ False

Tactic:
h0 _ (not_le.mp fun h ↦ hn (le_iff_exists_add'.mp h)) hk

Premises used: not_le, Iff.mp, le_iff_exists_add'
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
hn : ¬∃ (y : ℕ), k = y + m
⊢ False

Tactic:
exact h0 _ (not_le.mp fun h ↦ hn (le_iff_exists_add'.mp h)) hk

Premises used: not_le, Iff.mp, le_iff_exists_add'
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
rw : nth (fun (i : ℕ) ↦ p (i + m)) n = nth (fun (i : ℕ) ↦ p (i + m)) n + m - m
rw₁ rw₂ : nth (fun (i : ℕ) ↦ p (i + m)) n = nth (fun (i : ℕ) ↦ p (i + m)) n
⊢ nth (fun (i : ℕ) ↦ p (i + m)) n = nth p n - m

Tactic:
rw [← nth_add h0 h, Nat.add_sub_cancel]

Premises used: Nat.add_sub_cancel, Nat.nth_add
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h0 : ¬p 0
h : nth p n ≠ 0
⊢ nth (fun (i : ℕ) ↦ p (i + 1)) n + 1 = nth p n

Tactic:
nth_add (fun _ hk ↦ (lt_one_iff.1 hk ▸ h0)) h

Premises used: Eq.rec, Nat.lt_one_iff, Iff.mp, Eq.symm, Nat.nth_add
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
h0 : ¬p 0
h : nth p n ≠ 0
⊢ nth (fun (i : ℕ) ↦ p (i + 1)) n = nth p n - 1

Tactic:
nth_add_eq_sub (fun _ hk ↦ (lt_one_iff.1 hk ▸ h0)) h

Premises used: Eq.rec, Nat.lt_one_iff, Iff.mp, Eq.symm, Nat.nth_add_eq_sub
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
rw : ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x
⊢ count p (nth p 0) = 0

Tactic:
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]

Premises used: Nat.count_eq_card_filter_range, Nat.nth_zero, Finset.filter_eq_empty_iff, Finset.card_eq_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x

Tactic:
fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

Premises used: Finset.mem_range, Nat.sInf_le, Iff.mp, LT.lt.not_ge, Not
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x

Tactic:
exact fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

Premises used: Finset.mem_range, Nat.sInf_le, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k a : ℕ
ha : a ∈ {n ∈ range (nth p (k + 1)) | p n}
simp : ∀ (ha : a < nth p (k + 1) ∧ p a), a = nth p k ∨ a < nth p k ∧ p a
⊢ a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Premises used: Finset.mem_insert, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a

Tactic:
(le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩

Premises used: LE.le.eq_or_lt, And.right, And.left, And.intro, Nat.le_nth_of_lt_nth_succ, Or.imp_right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a

Tactic:
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩

Premises used: LE.le.eq_or_lt, And.right, And.left, Nat.le_nth_of_lt_nth_succ, Or.imp_right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
(filter_range_nth_subset_insert p k).antisymm fun a ha => ?_

Premises used: Nat.filter_range_nth_subset_insert, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
refine : ∀ (a : ℕ) (ha : a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})), a ∈ {n ∈ range (nth p (k + 1)) | p n}
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_

Premises used: Nat.filter_range_nth_subset_insert, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
a : ℕ
ha : a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
simp : ∀ (ha : a = nth p k ∨ a < nth p k ∧ p a), a < nth p (k + 1) ∧ p a
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n}

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Premises used: Finset.mem_insert, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ nth p k < nth p (k + 1)

Tactic:
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
this : nth p k < nth p (k + 1)
inl : nth p k < nth p (k + 1) ∧ p (nth p k)
inr : ∀ (hlt : a < nth p k) (hpa : p a), a < nth p (k + 1) ∧ p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
rcases ha with (rfl | ⟨hlt, hpa⟩)

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

Tactic:
⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩

Premises used: Nat.nth_mem, Nat.lt_succ_self, And.intro, LT.lt.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

Tactic:
exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩