awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
succ : Set.Nonempty (α := ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
⊢ f (n + 1) ≤ sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
have succ₁ : ∀ (b : ℕ), Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x} b → f (n + 1) ≤ b
Tactic: refine le_csInf ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
⊢ Set.Nonempty (α := ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
have right : ∀ k < n + 1, nth p k < nth p (n + 1)
Tactic: use nth p (n + 1), nth_mem _ hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
b : ℕ
hb : p b
h : ∀ k < n + 1, nth p k < b
⊢ f (n + 1) ≤ b
have succ : ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m)
  (hb : p (f m)) (h : ∀ k < n + 1, nth p k < f m), f (n + 1) ≤ f m
Tactic: rcases hsurj hb with ⟨m, hm, rfl⟩
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ f (n + 1) ≤ f m
have succ : n + 1 ≤ m
Tactic: apply hmono hn hm
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n < m
have succ : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n
Tactic: apply hmono.reflect_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n
hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
succ : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n
succ₁ : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m
⊢ n < m
have succ₂ : f n < f m
Tactic: apply hmono.reflect_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ f n ≤ nth p n
have zero : ∀ (hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))), f 0 ≤ nth p 0
Tactic: induction n with
  | zero =>
    rw [Nat.nth_zero]
    refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
    rcases hsurj hb with ⟨k, hk, rfl⟩
    exact hmono hn hk (Nat.zero_le _)
  | succ n ih =>
    rw [nth_eq_sInf]
    refine le_csInf ?_ ?_
    · use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn
    rintro b ⟨hb, h⟩
    rcases hsurj hb with ⟨m, hm, rfl⟩
    apply hmono hn hm
    rw [Nat.succ_le_iff]
    apply hmono.reflect_lt <;> grind
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : MonotoneOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
zero : ∀ (hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))), f 0 ≤ nth p 0
⊢ f n ≤ nth p n
have succ : ∀ (n : ℕ) (ih : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), f n ≤ nth p n)
  (hn : ∀ (hf : (setOf p).Finite), n + 1 < #(hf.toFinset (s := setOf p))), f (n + 1) ≤ nth p (n + 1)
Tactic: induction n with
  | zero =>
    rw [Nat.nth_zero]
    refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
    rcases hsurj hb with ⟨k, hk, rfl⟩
    exact hmono hn hk (Nat.zero_le _)
  | succ n ih =>
    rw [nth_eq_sInf]
    refine le_csInf ?_ ?_
    · use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn
    rintro b ⟨hb, h⟩
    rcases hsurj hb with ⟨m, hm, rfl⟩
    apply hmono hn hm
    rw [Nat.succ_le_iff]
    apply hmono.reflect_lt <;> grind
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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'
have h₁ : ∀ (i : ℕ), i ∈ f '' {i : ℕ | p' (f i)} ↔ i ∈ setOf p'
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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 : ℕ
⊢ i ∈ f '' {i : ℕ | p' (f i)} ↔ i ∈ setOf p'
have h₁ : ∀ (he : i ∈ setOf p'), i ∈ f '' {i : ℕ | p' (f i)}
Tactic: refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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'
⊢ i ∈ f '' {i : ℕ | p' (f i)}
have h₁ : ∀ (t : ℕ) (he : f t ∈ setOf p'), f t ∈ f '' {i : ℕ | p' (f i)}
Tactic: rcases h0p' _ he with ⟨t, rfl⟩
Cleared hypotheses: i, he
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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))
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) n) = nth p n
have hs : ∀ {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⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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'
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) n) = nth p n
have induction : ∀ (h : ∀ (hfi : (setOf p).Finite), 0 < #(hfi.toFinset (s := setOf p))), f (nth (fun (i : ℕ) ↦ p (f i)) 0) = nth p 0
Tactic: induction n using Nat.case_strong_induction_on
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) n) = nth p n
have 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)
Tactic: induction n using Nat.case_strong_induction_on
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
have simp_rw : f (sInf {i : ℕ | p (f i)}) = sInf (setOf p)
Tactic: simp_rw [nth_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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 (sInf {i : ℕ | p (f i)}) = sInf (setOf p)
have h₁ : p (nth p 0)
Tactic: replace h := nth_mem _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ f (sInf {i : ℕ | p (f i)}) = sInf (setOf p)
have rw : Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}
Tactic: rw [← hs h0, ← hf.monotone.map_csInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}
have rcases : ∀ (t : ℕ) (ht : f t = nth p 0), Set.Nonempty (α := ℕ) {i : ℕ | p (f i)}
Tactic: rcases h0 _ h with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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))
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) (n + 1)) = nth p (n + 1)
have nth_rw : 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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))
⊢ f (sInf {x : ℕ | p (f x) ∧ ∀ k < n + 1, nth (fun (i : ℕ) ↦ p (f i)) k < x}) = nth p (n + 1)
have 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}
Tactic: nth_rw 1 [nth_eq_sInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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))
⊢ f (nth (fun (i : ℕ) ↦ p (f i)) (n + 1)) = nth p (n + 1)
have 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}
Tactic: repeat nth_rw 1 [nth_eq_sInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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))
⊢ 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}
have h0' : ∀ (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
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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}) =
    sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
have 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})
Tactic: rw [← hs h0', ← hf.monotone.map_csInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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})
⊢ 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}
have rw₁ : Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}
Tactic: rw [← hs h0', ← hf.monotone.map_csInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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 {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i})
have h₁ : ∀ (k m' : ℕ) (hm : m' < n + 1), nth p m' < f k ↔ nth (fun (i : ℕ) ↦ p (f i)) m' < k
Tactic: convert! rfl using 8 with k m' hm
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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 (fun (i : ℕ) ↦ p (f i)) m' < k
have h₁ : nth p m' < f k ↔ f (nth (fun (i : ℕ) ↦ p (f i)) m') < f k
Tactic: nth_rw 2 [← hf.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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 ↔ f (nth (fun (i : ℕ) ↦ p (f i)) m') < f k
have h₁ : f (nth (fun (i : ℕ) ↦ p (f i)) m') = nth p m'
Tactic: convert! Iff.rfl using 2
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}
have rcases : ∀ (t : ℕ) (ht : f t = nth p (n + 1)), Set.Nonempty (α := ℕ) {i : ℕ | p (f i) ∧ ∀ k < n + 1, nth p k < f i}
Tactic: rcases h0 _ (nth_mem _ h) with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
have refine : ∀ (k : ℕ) (hk : p k), Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ id x + m) k
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)
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
k : ℕ
hk : p k
⊢ Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ id x + m) k
have by_contra : ∀ (hn : k ∉ Set.range fun (x : ℕ) ↦ id x + m), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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
⊢ False
have hn₁ : ¬∃ (y : ℕ), k = y + m
Tactic: simp_rw [id_eq, Set.mem_range, eq_comm] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun (i : ℕ) ↦ p (i + m)) n = nth p n - m
have rw : nth (fun (i : ℕ) ↦ p (i + m)) n = nth (fun (i : ℕ) ↦ p (i + m)) n + m - m
Tactic: rw [← nth_add h0 h, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth (fun (i : ℕ) ↦ p (i + m)) n = nth p n - m
have rw₁ : nth (fun (i : ℕ) ↦ p (i + m)) n = nth (fun (i : ℕ) ↦ p (i + m)) n
Tactic: rw [← nth_add h0 h, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ count p (nth p 0) = 0
have rw : ∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x
Tactic: rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
k a : ℕ
ha : a ∈ {n ∈ range (nth p (k + 1)) | p n}
⊢ a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
have simp : ∀ (ha : a < nth p (k + 1) ∧ p a), a = nth p k ∨ a < nth p k ∧ p a
Tactic: simp only [mem_insert, mem_filter, mem_range] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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})
have refine : ∀ (a : ℕ) (ha : a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})), a ∈ {n ∈ range (nth p (k + 1)) | p n}
Tactic: refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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})
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n}
have simp : ∀ (ha : a = nth p k ∨ a < nth p k ∧ p a), a < nth p (k + 1) ∧ p a
Tactic: simp only [mem_insert, mem_filter, mem_range] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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
⊢ a < nth p (k + 1) ∧ p a
have this : nth p k < nth p (k + 1)
Tactic: have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ a < nth p (k + 1) ∧ p a
have inl : nth p k < nth p (k + 1) ∧ p (nth p k)
Tactic: rcases ha with (rfl | ⟨hlt, hpa⟩)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ a < nth p (k + 1) ∧ p a
have inr : ∀ (hlt : a < nth p k) (hpa : p a), a < nth p (k + 1) ∧ p a
Tactic: rcases ha with (rfl | ⟨hlt, hpa⟩)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
ihk : ∀ (hn : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))), count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
⊢ count p (nth p (k + 1)) = k + 1
have succ : nth p k ∉ {n ∈ range (nth p k) | p n}
Tactic: rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]