Sets · hard

Statement, exactly as the model and Lean see it

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

Mathlib declaration: Set.Finite.exists_between
Held-out module: Mathlib.Data.Finset.DenselyOrdered
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 2 / 1

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.00011

Attempts

sample 0 · round 0Syntax error4.4 s model time

Proof

let b := Sup s
use b
· intro x
  intro hxs
  have hsup : x ≤ b := le_Sup hxs
  have hne : x ≠ b := by contraposition; intro h; rw [h] at hsup; exact not_le hsup
  exact lt_of_le_not_ge hsup hne
· intro y
  intro hyt
  have hinf : b ≤ y := le_Sup_iff.2 (hsf, ht, H, hyt)
  have hne : b ≠ y := by contraposition; intro h; rw [h] at hinf; exact not_le hinf
  exact lt_of_le_not_ge hinf hne

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

9:28: error: unknown tactic
4:11: error: Unknown identifier `Sup`
3:226: error: unsolved goals
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
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 Set.Finite.exists_between {s t : Set α}
    (hsf : s.Finite) (hs : s.Nonempty) (htf : t.Finite) (ht : t.Nonempty)
    (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ (∀ y ∈ t, b < y) := by
  convert!
    Finset.exists_between (s := hsf.toFinset) (t := htf.toFinset) (by simpa) (by simpa)
      (by simpa) using
    1; simp