awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
⊢ nth p a = 0

Tactic:
simp [nth_eq_zero, h']

Premises used: Nat.nth_eq_zero
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
⊢ nth p a = 0

Tactic:
have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
⊢ nth p b = 0

Tactic:
simp [nth_eq_zero, h'b]

Premises used: Nat.nth_eq_zero
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
⊢ nth p b = 0

Tactic:
have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
neg : p 0
⊢ p (nth p a)

Tactic:
rw [ha0]
-- 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
h'b : ∃ (hf : (setOf p).Finite), #(hf.toFinset (s := setOf p)) ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
neg neg₁ neg₂ neg₃ :
  ∀ (h : p 0) (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
⊢ p 0

Tactic:
rwa [hb0] at h
-- Module: Mathlib.Data.Nat.Nth
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
neg : ∀ (hn : ∃ (h : (setOf p).Finite), #(⋯.toFinset (s := setOf p)) ≤ n), nth p n ≤ f n
⊢ nth p n ≤ f n

Tactic:
by_cases! hn : (∀ hf : Set.Finite (setOf p), n < hf.toFinset.card)
-- Module: Mathlib.Data.Nat.Nth
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))
pos : sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x} ≤ f n
⊢ nth p n ≤ f n

Tactic:
rw [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
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))
⊢ BddBelow (α := ℕ) {x : ℕ | p x ∧ ∀ k < n, nth p k < x}

Tactic:
simp
-- Module: Mathlib.Data.Nat.Nth
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))
pos : ∀ (k : ℕ) (hk : k < n), nth p k < f n
⊢ sInf {x : ℕ | p x ∧ ∀ k < n, nth p k < x} ≤ f n

Tactic:
refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
-- Module: Mathlib.Data.Nat.Nth
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
x₁ : Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n
a : k < n
⊢ f k < f n

Tactic:
apply hmono
-- Module: Mathlib.Data.Nat.Nth
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
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} k

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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
⊢ k < n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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

Tactic:
have : f k < f n := by apply hmono <;> grind
-- Module: Mathlib.Data.Nat.Nth
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
this : f k < f n
⊢ nth p k < f n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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))
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
⊢ 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

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
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
⊢ (setOf p).Finite

Tactic:
rcases hn with ⟨hf, hn⟩
-- Module: Mathlib.Data.Nat.Nth
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
⊢ #(⋯.toFinset (s := setOf p)) ≤ n

Tactic:
rcases hn with ⟨hf, hn⟩
-- Module: Mathlib.Data.Nat.Nth
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
⊢ (hf.toFinset (s := setOf p).sort fun (a b : ℕ) ↦ a ≤ b).length ≤ n

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Nth
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
neg : 0 ≤ f n
⊢ nth p n ≤ f n

Tactic:
rw [nth, dif_pos hf, List.getD_eq_default _ _ (by simp [hn])]

Premises used: dif_pos, List.getD_eq_default, Nat.nth
-- Module: Mathlib.Data.Nat.Nth
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
⊢ 0 ≤ f n

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Nth
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
⊢ 0 ≤ f n

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Nth
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))
zero : f 0 ≤ sInf (setOf p)
⊢ f 0 ≤ nth p 0

Tactic:
rw [Nat.nth_zero]

Premises used: Nat.nth_zero
-- Module: Mathlib.Data.Nat.Nth
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)

Tactic:
le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_

Premises used: Nat.nth_mem, le_csInf, Exists.intro
-- Module: Mathlib.Data.Nat.Nth
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))
zero : ∀ (b : ℕ) (hb : b ∈ setOf p), f 0 ≤ b
⊢ f 0 ≤ sInf (setOf p)

Tactic:
refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_

Premises used: Nat.nth_mem, le_csInf, Exists.intro
-- Module: Mathlib.Data.Nat.Nth
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
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
⊢ f 0 ≤ b

Tactic:
rcases hsurj hb with ⟨k, hk, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
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))
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:
hmono hn hk (Nat.zero_le _)

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Nth
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))
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:
exact hmono hn hk (Nat.zero_le _)

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Nth
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 : f (n + 1) ≤ sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}
⊢ f (n + 1) ≤ nth p (n + 1)

Tactic:
rw [nth_eq_sInf]

Premises used: Nat.nth_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
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}

Tactic:
le_csInf ?_ ?_

Premises used: le_csInf
-- Module: Mathlib.Data.Nat.Nth
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}
succ₁ : ∀ (b : ℕ), Membership.mem (γ := Set ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x} b → f (n + 1) ≤ b
⊢ f (n + 1) ≤ sInf {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}

Tactic:
refine le_csInf ?_ ?_

Premises used: le_csInf
-- Module: Mathlib.Data.Nat.Nth
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))
right : ∀ k < n + 1, nth p k < nth p (n + 1)
⊢ Set.Nonempty (α := ℕ) {x : ℕ | p x ∧ ∀ k < n + 1, nth p k < x}

Tactic:
use nth p (n + 1), nth_mem _ hn

Premises used: Nat.nth_mem, HAdd.hAdd, Nat.nth, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Nth
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))
⊢ ∀ k < n + 1, nth p k < nth p (n + 1)

Tactic:
fun k hk => nth_lt_nth' hk hn

Premises used: Nat.nth_lt_nth'
-- Module: Mathlib.Data.Nat.Nth
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))
⊢ ∀ k < n + 1, nth p k < nth p (n + 1)

Tactic:
exact fun k hk => nth_lt_nth' hk hn

Premises used: Nat.nth_lt_nth'
-- Module: Mathlib.Data.Nat.Nth
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
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
⊢ f (n + 1) ≤ b

Tactic:
rcases hsurj hb with ⟨m, hm, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Nth
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 : n + 1 ≤ m
⊢ f (n + 1) ≤ f m

Tactic:
apply hmono hn hm
-- Module: Mathlib.Data.Nat.Nth
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
succ₂ : f n < f m
⊢ n < m

Tactic:
apply hmono.reflect_lt

Premises used: MonotoneOn.reflect_lt
-- Module: Mathlib.Data.Nat.Nth
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
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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 < f m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Nth
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
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)
⊢ f n ≤ nth p n

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

Premises used: MonotoneOn.reflect_lt, Nat.nth_mem, le_csInf, Nat.nth_zero, Nat.nth_eq_sInf, Nat.nth_lt_nth', HAdd.hAdd, Exists.intro, Nat.zero, Nat.nth, OfNat.ofNat, Nat.succ_le_iff, Nat.succ, rfl
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))} (setOf p)
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))}
⊢ Set.EqOn f (nth p) {n : ℕ | ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))}

Tactic:
fun _ hi => le_antisymm
    (Nat.le_nth_of_monotoneOn_of_surjOn _ hsurj hmono.monotoneOn hi)
    (Nat.nth_le_of_strictMonoOn_of_mapsTo _ hmaps hmono)

Premises used: Nat.nth_le_of_strictMonoOn_of_mapsTo, Set.EqOn, le_antisymm, StrictMonoOn.monotoneOn, Nat.le_nth_of_monotoneOn_of_surjOn
-- 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
h₁ : ∀ (i : ℕ), i ∈ f '' {i : ℕ | p' (f i)} ↔ i ∈ setOf p'
⊢ f '' {i : ℕ | p' (f i)} = setOf p'

Tactic:
ext i
-- 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 : ℕ
⊢ i ∈ f '' {i : ℕ | p' (f i)} ↔ i ∈ setOf p'

Tactic:
⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩

Premises used: _private.0.Nat.nth_comp_of_strictMono.match_1, setOf, Membership.mem, Eq.rec, Iff.intro