Sets · hard

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} [LinearOrder α] [DenselyOrdered α] (s t : Finset α) [NoMaxOrder α] [NoMinOrder α] [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): 8 / 1

Traces

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

Verified2 model calls · 2 Lean checks · $0.00044

Retrieved lemmas

1. Order.exists_between_finsets
2. Finset.exists_next_right
3. Finset.exists_next_left
4. Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt
5. Finset.lt_fold_min
6. Finset.Colex.toColex_lt_toColex
7. Finset.min'_eq_iff
8. dense_or_discrete

Plan

### Explanation of the Proof: The theorem states that given two non-empty, disjoint finite sets `s` and `t` of a densely ordered linearly ordered type `α` with no minimum or maximum, and such that every element of `s` is less than every element of `t`, there exists an element `b` that lies strictly between all elements of `s` and all elements of `t`. This is essentially a version of the **density of order** in between two disjoint sets. The key idea is to use the fact that the order is dense and has no endpoints, so we can always find an element between any two such sets. The relevant Mathlib lemma `Order.exists_between_finsets` directly provides this result under the given assumptions, so the proof is relatively straightforward: simply apply that lemma. --- ### Lean 4 Proof Skeleton This proof skeleton uses the direct Mathlib lemma `Order.exists_between_finsets` which is precisely the statement of the theorem. The rest is just unpacking the result.

Skeleton — Lean reported problems

import Order.Lattice
import Data.Finset

open Finset

theorem lg_target {α : Type u_1} [LinearOrder α] [DenselyOrdered α] (s t : Finset α)
  [NoMaxOrder α] [NoMinOrder α] [Nonempty α]
  (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y :=
by
  have : ∃ m, (∀ x ∈ s, x < m) ∧ ∀ y ∈ t, m < y :=
    Order.exists_between_finsets s t H
  exact this

Attempts

sample 0 · round 0Verified1.7 s model time
Proof
```
exact Order.exists_between_finsets s t H
```

Verified proof

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

Axioms used: propext, Classical.choice, Quot.sound

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 α) [NoMaxOrder α] [NoMinOrder α] [Nonempty α]
    (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ (∀ y ∈ t, b < y) := by
  by_cases hs : s.Nonempty <;> by_cases ht : t.Nonempty
  · exact s.exists_between hs ht H
  · exact let ⟨p, hp⟩ := exists_gt (s.max' hs); ⟨p, by simp_all⟩
  · exact let ⟨p, hp⟩ := exists_lt (t.min' ht); ⟨p, by simp_all⟩
  · exact Nonempty.elim ‹_› fun p ↦ ⟨p, by simp_all⟩