awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
have refine_1 : ∀ (hf : (setOf p).Finite), ∃ (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 => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
have refine_2 : ∀ (hf : (setOf p).Infinite), ∃ (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 => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Finite
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
have 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
Tactic: rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
x : ℕ
h : p x
hf : (setOf p).Infinite
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
have h₁ : x ∈ Set.range (nth p)
Tactic: rw [← @Set.mem_setOf_eq _ _ p, ← range_nth_of_infinite hf] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : (setOf p).Infinite
⊢ ∃ (n : ℕ), (∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))) ∧ nth p n = x
have refine_2 : ∀ (n : ℕ) (hx : 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⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
have 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}
Tactic: by_cases! hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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}
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
have neg : ∀ (hn : ∃ (h : (setOf p).Finite), #(sorry.toFinset (s := setOf p)) ≤ n), nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
Tactic: by_cases! hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
have hf : (setOf p).Finite
Tactic: rcases hn with ⟨hf, hn⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
hf : (setOf p).Finite
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
have hn₁ : #(sorry.toFinset (s := setOf p)) ≤ n
Tactic: rcases hn with ⟨hf, hn⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
⊢ nth p n = sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x}
have neg : Eq (α := ℕ) 0 (sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x})
Tactic: rw [nth_of_card_le _ hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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})
have neg : ∀ (k : ℕ) (hk : Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x} k), False
Tactic: refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ False
have 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
Tactic: rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
⊢ nth p 0 = sInf (setOf p)
have rw : sInf {x : ℕ | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)
Tactic: rw [nth_eq_sInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ nth p 0 = Nat.find (p := p) h
have rw : sInf (setOf p) = Nat.find (p := p) h
Tactic: rw [nth_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
hf : (setOf p).Finite
⊢ n < #(hf.toFinset (s := setOf p))
have h₁ : ¬(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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0
have simp : ∀ (ha : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ a),
  ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
Tactic: simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k
have inl : ∀ (hf : (setOf p).Finite), a ≤ nth p k
Tactic: rcases (setOf p).finite_or_infinite with hf | hf
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
inl : ∀ (hf : (setOf p).Finite), a ≤ nth p k
⊢ a ≤ nth p k
have inr : ∀ (hf : (setOf p).Infinite), a ≤ nth p k
Tactic: rcases (setOf p).finite_or_infinite with hf | hf
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Finite
⊢ a ≤ nth p k
have 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
Tactic: rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ nth p n ≤ nth p k
have inl : ∀ (hk : k + 1 < #(hf.toFinset (s := setOf p))), nth p n ≤ nth p k
Tactic: rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth p n ≤ nth p k
have inl₁ : ∀ (hk : #(hf.toFinset (s := setOf p)) ≤ k + 1), nth p n ≤ nth p k
Tactic: rcases lt_or_ge (k + 1) #hf.toFinset with hk | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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))
⊢ nth p n ≤ nth p k
have inl : ∀ (h : n < k + 1) (ha : p (nth p n)) (hk : k + 1 < #(hf.toFinset (s := setOf p))), 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
Cleared hypotheses: h, ha, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth p n ≤ nth p k
have inl₁ : ∀ (h : n ≤ k) (ha : p (nth p n)) (hk : k + 1 < #(hf.toFinset (s := setOf p))), 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
Cleared hypotheses: h, ha, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth p n ≤ nth p k
have 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
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
Cleared hypotheses: h, ha, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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 ≤ nth p k
have h₁ : nth p n < 0
Tactic: rw [nth_of_card_le _ hk] at h
Cleared hypotheses: h, ha, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Infinite
⊢ a ≤ nth p k
have inr : ∀ (n : ℕ) (h : nth p n < nth p (k + 1)) (ha : p (nth p n)), nth p n ≤ nth p k
Tactic: rcases subset_range_nth ha with ⟨n, rfl⟩
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
k : ℕ
hf : (setOf p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
have inr : ∀ (h : n < k + 1) (ha : p (nth p n)), nth p n ≤ nth p k
Tactic: rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth p n ≤ nth p k
have inr₁ : ∀ (h : n ≤ k) (ha : p (nth p n)), nth p n ≤ nth p k
Tactic: rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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
⊢ nth p n ≤ nth p k
have inr₂ : ∀ (h : nth p n ≤ nth p k) (ha : p (nth p n)), nth p n ≤ nth p k
Tactic: rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
⊢ p (nth p a)
have pos : ∀ (h' : ∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))), p (nth p a)
Tactic: by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
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)
⊢ p (nth p a)
have neg : ∀ (h' : ¬∀ (hf : (setOf p).Finite), a < #(hf.toFinset (s := setOf p))), p (nth p a)
Tactic: by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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)
have h'₁ : ∃ (h : (setOf p).Finite), #(sorry.toFinset (s := setOf p)) ≤ a
Tactic: simp only [not_forall, not_lt] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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), #(hf.toFinset (s := setOf p)) ≤ b
have hf : (setOf p).Finite
Tactic: rcases h' with ⟨hf, ha⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
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
⊢ ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
have ha : #(sorry.toFinset (s := setOf p)) ≤ a
Tactic: rcases h' with ⟨hf, ha⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
⊢ p (nth p a)
have neg : ∀ (h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b), 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⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
⊢ p (nth p a)
have ha0 : nth p a = 0
Tactic: have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
⊢ p (nth p a)
have hb0 : nth p b = 0
Tactic: have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p (nth p a)
have neg : p 0
Tactic: rw [ha0]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ a
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p 0
have neg : ∀ (h : p 0) (h' : ∃ (h : (setOf p).Finite), #(sorry.toFinset (s := setOf p)) ≤ a)
  (h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b) (ha0 : nth p a = 0) (hb0 : nth p b = 0), p 0
Tactic: rwa [hb0] at h
Cleared hypotheses: h, h', h'b, ha0, hb0
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
⊢ nth p n ≤ f n
have pos : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), nth p n ≤ f n
Tactic: by_cases! hn : (∀ hf : Set.Finite (setOf p), n < hf.toFinset.card)
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
pos : ∀ (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), nth p n ≤ f n
⊢ nth p n ≤ f n
have neg : ∀ (hn : ∃ (h : (setOf p).Finite), #(sorry.toFinset (s := setOf p)) ≤ n), nth p n ≤ f n
Tactic: by_cases! hn : (∀ hf : Set.Finite (setOf p), n < hf.toFinset.card)
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p n ≤ f n
have pos : sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x} ≤ f n
Tactic: rw [nth_eq_sInf]
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x} ≤ f n
have pos : ∀ (k : ℕ) (hk : k < n), nth p k < f n
Tactic: refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
k : ℕ
hk : k < n
⊢ f k < f n
have x : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} k
Tactic: apply hmono
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
k : ℕ
hk : k < n
x : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} k
⊢ f k < f n
have x₁ : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n
Tactic: apply hmono
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
k : ℕ
hk : k < n
⊢ nth p k < f n
have this : f k < f n
Tactic: have : f k < f n := by apply hmono <;> grind
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
⊢ nth p n ≤ f n
have pos : ∀ (n : ℕ) (ih : ∀ m < n, ∀ (hn : ∀ (hf : (setOf p).Finite), m < #(hf.toFinset (s := setOf p))), nth p m ≤ f m)
  (hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))), nth p n ≤ f n
Tactic: induction n using Nat.strong_induction_on with | _ n ih =>
    rw [nth_eq_sInf]
    refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
    have : f k < f n := by apply hmono <;> grind
    grind
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
⊢ nth p n ≤ f n
have hf : (setOf p).Finite
Tactic: rcases hn with ⟨hf, hn⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (hypothesis)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n
hf : (setOf p).Finite
⊢ nth p n ≤ f n
have hn₁ : #(sorry.toFinset (s := setOf p)) ≤ n
Tactic: rcases hn with ⟨hf, hn⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Nth (goal)
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
hmono : StrictMonoOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}
n : ℕ
hf : (setOf p).Finite
hn : #(⋯.toFinset (s := setOf p)) ≤ n
⊢ nth p n ≤ f n
have neg : 0 ≤ f n
Tactic: rw [nth, dif_pos hf, List.getD_eq_default _ _ (by simp [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))}
hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))
⊢ f 0 ≤ nth p 0
have zero : f 0 ≤ sInf (setOf p)
Tactic: rw [Nat.nth_zero]
-- 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))}
hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))
⊢ f 0 ≤ sInf (setOf p)
have zero : ∀ (b : ℕ) (hb : b ∈ setOf p), f 0 ≤ b
Tactic: refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
-- 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))}
hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))
b : ℕ
hb : b ∈ setOf p
⊢ f 0 ≤ b
have zero : ∀ (k : ℕ) (hk : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} k)
  (hb : f k ∈ setOf p), f 0 ≤ f k
Tactic: rcases hsurj hb with ⟨k, hk, rfl⟩
Cleared hypotheses: b, hb
-- 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))
⊢ f (n + 1) ≤ nth p (n + 1)
have succ : f (n + 1) ≤ sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
Tactic: rw [nth_eq_sInf]
-- 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))
⊢ f (n + 1) ≤ sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
have succ : Set.Nonempty (α := ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
Tactic: refine le_csInf ?_ ?_