[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ ℕ
[PROOFSTEP]
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
[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ ℕ
[PROOFSTEP]
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
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : card (Set.Finite.toFinset hf) ≤ n
⊢ nth p n = 0
[PROOFSTEP]
rw [nth, dif_pos hf, List.getD_eq_default]
[GOAL]
case hn
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : card (Set.Finite.toFinset hf) ≤ n
⊢ List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) ≤ n
[PROOFSTEP]
rwa [Finset.length_sort]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ nth p n =
    ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
      { val := n, isLt := hn }
[PROOFSTEP]
rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ List.get (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) { val := n, isLt := ?hn } =
    List.nthLe (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)) ↑{ val := n, isLt := hn }
      (_ : ↑{ val := n, isLt := hn } < List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf)))
case hn
p : ℕ → Prop
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
⊢ n < List.length (sort (fun x x_1 => x ≤ x_1) (Set.Finite.toFinset hf))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ StrictMonoOn (nth p) (Set.Iio (card (Set.Finite.toFinset hf)))
[PROOFSTEP]
rintro m (hm : m < _) n (hn : n < _) h
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
m : ℕ
hm : m < card (Set.Finite.toFinset hf)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : m < n
⊢ nth p m < nth p n
[PROOFSTEP]
simp only [nth_eq_orderEmbOfFin, *]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
m : ℕ
hm : m < card (Set.Finite.toFinset hf)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : m < n
⊢ ↑(orderEmbOfFin (Set.Finite.toFinset (_ : Set.Finite (setOf p)))
          (_ :
            card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) =
              card (Set.Finite.toFinset (_ : Set.Finite (setOf p)))))
      { val := m, isLt := (_ : m < card (Set.Finite.toFinset hf)) } <
    ↑(orderEmbOfFin (Set.Finite.toFinset (_ : Set.Finite (setOf p)))
          (_ :
            card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) =
              card (Set.Finite.toFinset (_ : Set.Finite (setOf p)))))
      { val := n, isLt := (_ : n < card (Set.Finite.toFinset hf)) }
[PROOFSTEP]
exact OrderEmbedding.strictMono _ h
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ Set.range (nth p) = insert 0 (setOf p)
[PROOFSTEP]
simpa only [← nth_eq_getD_sort hf, mem_sort, Set.Finite.mem_toFinset] using
  Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ nth p '' Set.Iio (card (Set.Finite.toFinset hf)) =
    Set.range
      ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
[PROOFSTEP]
ext x
[GOAL]
case h
p : ℕ → Prop
hf : Set.Finite (setOf p)
x : ℕ
⊢ x ∈ nth p '' Set.Iio (card (Set.Finite.toFinset hf)) ↔
    x ∈
      Set.range
        ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf)))
[PROOFSTEP]
simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf, Set.mem_Iio, exists_prop]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
⊢ Set.range
      ↑(orderEmbOfFin (Set.Finite.toFinset hf) (_ : card (Set.Finite.toFinset hf) = card (Set.Finite.toFinset hf))) =
    setOf p
[PROOFSTEP]
rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]
[GOAL]
p : ℕ → Prop
hf : Set.Finite (setOf p)
x : ℕ
h : p x
⊢ ∃ n, n < card (Set.Finite.toFinset hf) ∧ nth p n = x
[PROOFSTEP]
rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h 
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
n : ℕ
⊢ nth p n = ↑(↑(Subtype.orderIsoOfNat (setOf p)) n)
[PROOFSTEP]
rw [nth, dif_neg hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ StrictMono (nth p)
[PROOFSTEP]
rw [nth_eq_orderIsoOfNat hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ StrictMono (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p)))
[PROOFSTEP]
exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ Set.range (nth p) = setOf p
[PROOFSTEP]
rw [nth_eq_orderIsoOfNat hf]
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
haveI := hf.to_subtype
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
classical exact Nat.Subtype.coe_comp_ofNat_range
[GOAL]
p : ℕ → Prop
hf : Set.Infinite (setOf p)
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ↑(Subtype.orderIsoOfNat (setOf p))) = setOf p
[PROOFSTEP]
exact Nat.Subtype.coe_comp_ofNat_range
[GOAL]
p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
refine' (setOf p).finite_or_infinite.elim (fun hf => _) fun hf => _
[GOAL]
case refine'_1
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Finite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
[GOAL]
case refine'_1.intro.intro
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
hx : nth p n = x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
exact ⟨n, fun _ => hn, hx⟩
[GOAL]
case refine'_2
p : ℕ → Prop
x : ℕ
h : p x
hf : Set.Infinite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h 
[GOAL]
case refine'_2
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : Set.Infinite (setOf p)
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
rcases h with ⟨n, hx⟩
[GOAL]
case refine'_2.intro
p : ℕ → Prop
x : ℕ
hf : Set.Infinite (setOf p)
n : ℕ
hx : nth p n = x
⊢ ∃ n, (∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)) ∧ nth p n = x
[PROOFSTEP]
exact ⟨n, fun hf' => absurd hf' hf, hx⟩
[GOAL]
p✝ p : ℕ → Prop
n : ℕ
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
by_cases hn : ∀ hf : (setOf p).Finite, n < hf.toFinset.card
[GOAL]
case pos
p✝ p : ℕ → Prop
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
exact (isLeast_nth hn).csInf_eq.symm
[GOAL]
case neg
p✝ p : ℕ → Prop
n : ℕ
hn : ¬∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
push_neg at hn 
[GOAL]
case neg
p✝ p : ℕ → Prop
n : ℕ
hn : ∃ h, card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
rcases hn with ⟨hf, hn⟩
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
rw [nth_of_card_le _ hn]
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
⊢ 0 = sInf {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
[PROOFSTEP]
refine' ((congr_arg sInf <| Set.eq_empty_of_forall_not_mem fun k hk => _).trans sInf_empty).symm
[GOAL]
case neg.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
k : ℕ
hk : k ∈ {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
⊢ False
[PROOFSTEP]
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
[GOAL]
case neg.intro.intro.intro
p✝ p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hn : card (Set.Finite.toFinset (_ : Set.Finite (setOf p))) ≤ n
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)
hk : nth p k ∈ {x | p x ∧ ∀ (k : ℕ), k < n → nth p k < x}
⊢ False
[PROOFSTEP]
exact (hk.2 _ ((hlt hf).trans_le hn)).false
[GOAL]
p : ℕ → Prop
⊢ nth p 0 = sInf (setOf p)
[PROOFSTEP]
rw [nth_eq_sInf]
[GOAL]
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ (k : ℕ), k < 0 → nth p k < x} = sInf (setOf p)
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0
[PROOFSTEP]
simp [nth_zero, h]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ nth p 0 = Nat.find h
[PROOFSTEP]
rw [nth_zero]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (setOf p) = Nat.find h
[PROOFSTEP]
convert Nat.sInf_def h
[GOAL]
p : ℕ → Prop
n : ℕ
⊢ nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n
[PROOFSTEP]
simp only [or_iff_not_imp_right, not_exists, not_le]
[GOAL]
case refine'_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ (∀ (x : Set.Finite (setOf p)), n < card (Set.Finite.toFinset x)) → p 0 ∧ n = 0
[PROOFSTEP]
exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩
[GOAL]
case refine'_2
p : ℕ → Prop
n : ℕ
⊢ (p 0 ∧ n = 0 ∨ ∃ hf, card (Set.Finite.toFinset hf) ≤ n) → nth p n = 0
[PROOFSTEP]
rintro (⟨h₀, rfl⟩ | ⟨hf, hle⟩)
[GOAL]
case refine'_2.inl.intro
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0
case refine'_2.inr.intro
p : ℕ → Prop
n : ℕ
hf : Set.Finite (setOf p)
hle : card (Set.Finite.toFinset hf) ≤ n
⊢ nth p n = 0
[PROOFSTEP]
exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]
[GOAL]
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0
[PROOFSTEP]
simp only [nth_eq_zero, h₀, false_and_iff, false_or_iff] at ha ⊢
[GOAL]
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ hf, card (Set.Finite.toFinset hf) ≤ a
⊢ ∃ hf, card (Set.Finite.toFinset hf) ≤ b
[PROOFSTEP]
exact ha.imp fun hf hle => hle.trans hab
[GOAL]
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k
[PROOFSTEP]
cases' (setOf p).finite_or_infinite with hf hf
[GOAL]
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : Set.Finite (setOf p)
⊢ a ≤ nth p k
[PROOFSTEP]
rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
[GOAL]
case inl.intro.intro
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
cases' lt_or_le (k + 1) hf.toFinset.card with hk hk
[GOAL]
case inl.intro.intro.inl
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < card (Set.Finite.toFinset hf)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, lt_succ_iff, ←
  (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h 
[GOAL]
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : card (Set.Finite.toFinset hf) ≤ k + 1
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rw [nth_of_card_le _ hk] at h 
[GOAL]
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : Set.Finite (setOf p)
n : ℕ
hn : n < card (Set.Finite.toFinset hf)
h : nth p n < 0
ha : p (nth p n)
hk : card (Set.Finite.toFinset hf) ≤ k + 1
⊢ nth p n ≤ nth p k
[PROOFSTEP]
exact absurd h (zero_le _).not_lt
[GOAL]
case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : Set.Infinite (setOf p)
⊢ a ≤ nth p k
[PROOFSTEP]
rcases subset_range_nth ha with ⟨n, rfl⟩
[GOAL]
case inr.intro
p : ℕ → Prop
k : ℕ
hf : Set.Infinite (setOf p)
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
[PROOFSTEP]
rwa [nth_lt_nth hf, lt_succ_iff, ← nth_le_nth hf] at h 
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0
[PROOFSTEP]
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : ℕ), x ∈ range (sInf (setOf p)) → ¬p x
[PROOFSTEP]
exact fun n h₁ h₂ => (mem_range.1 h₁).not_le (Nat.sInf_le h₂)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ filter p (range (nth p (k + 1))) ⊆ insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
intro a ha
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ filter p (range (nth p (k + 1)))
⊢ a ∈ insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
[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
[PROOFSTEP]
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
⊢ filter p (range (nth p (k + 1))) = insert (nth p k) (filter p (range (nth p k)))
[PROOFSTEP]
refine' (filter_range_nth_subset_insert p k).antisymm fun a ha => _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
ha : a ∈ insert (nth p k) (filter p (range (nth p k)))
⊢ a ∈ filter p (range (nth p (k + 1)))
[PROOFSTEP]
simp only [mem_insert, mem_filter, mem_range] at ha ⊢
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a
[PROOFSTEP]
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
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
[PROOFSTEP]
rcases ha with (rfl | ⟨hlt, hpa⟩)
[GOAL]
case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)
[PROOFSTEP]
exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩
[GOAL]
case inr.intro
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : Set.Finite (setOf p)), k + 1 < card (Set.Finite.toFinset hf)
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a
[PROOFSTEP]
exact ⟨hlt.trans this, hpa⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ count p (nth p n) = n
[PROOFSTEP]
induction' n with k ihk
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
hn : ∀ (hf : Set.Finite (setOf p)), zero < card (Set.Finite.toFinset hf)
⊢ count p (nth p zero) = zero
[PROOFSTEP]
exact count_nth_zero _
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
k : ℕ
ihk : (∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)) → count p (nth p k) = k
hn : ∀ (hf : Set.Finite (setOf p)), succ k < card (Set.Finite.toFinset hf)
⊢ count p (nth p (succ k)) = succ k
[PROOFSTEP]
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_not_mem, ← count_eq_card_filter_range,
  ihk fun hf => lt_of_succ_lt (hn hf)]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn✝ : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
k : ℕ
ihk : (∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)) → count p (nth p k) = k
hn : ∀ (hf : Set.Finite (setOf p)), succ k < card (Set.Finite.toFinset hf)
⊢ ¬nth p k ∈ filter p (range (nth p k))
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : Set.Finite (setOf p)), n < card (Set.Finite.toFinset hf)
⊢ count p (nth p n + 1) = n + 1
[PROOFSTEP]
rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n
[PROOFSTEP]
refine' (count_monotone p).reflect_lt _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n
[PROOFSTEP]
rwa [count_nth]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : Set.Finite (setOf p)), k < card (Set.Finite.toFinset hf)
[PROOFSTEP]
exact fun hf => h.trans_le (count_le_card hf n)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i | p i ∧ n ≤ i}
[PROOFSTEP]
refine' (nth_eq_sInf _ _).trans (congr_arg sInf _)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ {x | p x ∧ ∀ (k : ℕ), k < count p n → nth p k < x} = {i | p i ∧ n ≤ i}
[PROOFSTEP]
refine' Set.ext fun a => and_congr_right fun hpa => _
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ (k : ℕ), k < count p n → nth p k < a) ↔ n ≤ a
[PROOFSTEP]
refine' ⟨fun h => not_lt.1 fun ha => _, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ (k : ℕ), k < count p n → nth p k < a
ha : a < n
⊢ False
[PROOFSTEP]
have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ (k : ℕ), k < count p n → nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False
[PROOFSTEP]
rwa [nth_count hpa, lt_self_iff_false] at hn 
