Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {β : Type u_1} [LinearOrder β] {t : ℕ → β} (ht_mono : StrictMono t) (ht_tendsto : Filter.Tendsto t Filter.atTop Filter.atTop) {x : β} (hx : t 0 < x) : ∃ n, t n < x ∧ x ≤ t (n + 1) := by

Mathlib declaration: StrictMono.exists_between_of_tendsto_atTop
Held-out module: Mathlib.Probability.Distributions.Fernique
Banned modules (itself + downstream): 11
Reference proof premises (reachable / held-out): 24 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00008

Attempts

sample 0 · round 0Syntax error6.5 s model time

Proof

let n := 0 in
let m := 0 in
let h0 : t 0 < x := hx,
let h1 : x ≤ t (n + 1) := Filter.Tendsto.eventually_le ht_tendsto (le_rfl x) (lt_iff_le_and_gt.2 h0).2,
constructor,
exact h0,
exact h1

What Lean printed (this is all the model sees on repair)

4:15: error: unexpected token 'let'; expected command
3:201: error: unsolved goals
β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Filter.Tendsto t Filter.atTop Filter.atTop
x : β
hx : t 0 < x
n : ℕ := 0
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma StrictMono.exists_between_of_tendsto_atTop {β : Type*} [LinearOrder β] {t : ℕ → β}
    (ht_mono : StrictMono t) (ht_tendsto : Tendsto t atTop atTop) {x : β} (hx : t 0 < x) :
    ∃ n, t n < x ∧ x ≤ t (n + 1) := by
  have h : ∃ n, x ≤ t n := by
    simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
    exact ht_tendsto x
  have h' m := Nat.find_min h (m := m)
  simp only [not_le] at h'
  exact ⟨Nat.find h - 1, h' _ (by simp [hx]), by simp [Nat.find_spec h, hx]⟩