Sets · medium

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} [LinearOrder α] [DenselyOrdered α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y := by

Mathlib declaration: Finset.exists_between
Held-out module: Mathlib.Data.Finset.DenselyOrdered
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 3 / 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.00010

Attempts

sample 0 · round 0Hallucinated theorem7.6 s model time

Proof

let b := Sup s
use b
· intro x
  intro hx
  have h1 : x ∈ s := hx
  have h2 : x ≤ b := le_Sup_iff.1 (mem_Sup h1)
  rw [le_antisymm_iff] at h2
  exact h2.1
· intro y
  intro hy
  have h1 : y ∈ t := hy
  have h2 : b ≤ y := le_Sup_iff.2 (mem_Sup h1)
  rw [le_antisymm_iff] at h2
  exact h2.2

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

4:11: error: Unknown identifier `Sup`
3:195: error: unsolved goals
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Reference proof

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

theorem Finset.exists_between {s t : Finset α}
    (hs : s.Nonempty) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) :
    ∃ b, (∀ x ∈ s, x < b) ∧ (∀ y ∈ t, b < y) := by
  convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all) <;> simp