How to declare a supremum

Stream: general

[W.P. McNeill]

I'm new to Lean. Teaching myself by working through basic theorems with the help of the documentation and CoPilot.

I'm trying to write a proof for the Nested Interval Property from analysis. This requires identifying the supremum and infinitum of two different sets. I am trying to work with the supremum. I've got this far.

import Mathlib.Data.Real.Basic

--1.4 Consequences of Completeness

--Theorem 1.4.1
def I (a b : ℕ → ℝ) (n: ℕ) : Set ℝ := {x | a n ≤ x ∧ x ≤ b n}

theorem nested_interval_property
  (a b : ℕ → ℝ)
  (nested : ∀ n, I a b (n + 1) ⊆ I a b n)
  (b0_upper_bound: ∀ n, a n ≤ b 0 := by sorry):
  (⋂ n, I a b n).Nonempty :=
  by
    let A : Set ℝ := {x | ∃ n, x = a n}
    have A_nonempty : A.Nonempty := by
      use a 0
      exact ⟨0, rfl⟩
    have A_bounded : BddAbove A := by
      use b 0
      rintro x ⟨n, rfl⟩
      exact b0_upper_bound n
    let a' := sSup A

The last line has a "failed to synthesize" error. I think that means that Lean doesn't think I have proved that A has a supremum despite the two previous have blocks.

Usually CoPilot can get me past these syntax errors, but it's going in circles, telling me to import packages and then telling me to remove them again.

1. How do I make this line work?
2. How could I go about debugging this problem besides asking CoPilot?

Thanks.

[Weiyi Wang]

You can resolve the error by importing the entire mathlib

import Mathlib
...

[Weiyi Wang]

When initially exploring, it is often a good idea to import the whole thing, because instances might be scattered at places that you are not familiar with yet. Later you can use #min_imports to minimize the import

[Weiyi Wang]

Oh, and the error isn't because the lean thinks you didn't prove certain things in this case. It is just because it doesn't know how to do sup with Real by only looking at Mathlib.Data.Real.Basic. That operation is defined somewhere else

[Weiyi Wang]

It should be also noted that sSup is a "total function with junk value", meaning that it doesn't require hypothesis to use (non-emptiness or boundedness), but it will give junk output for those edge cases (I think it is 0 for those)

[W.P. McNeill]

import Mathlib fixed it.

As a rule of thumb, does "failed to synthesize" mean I'm missing an import?

[W.P. McNeill]

On paper I would write a' = sup A. Is there a best way to write this in Lean at this point?

[Weiyi Wang]

"failed to synthesize" usually is one of the following things

• Missing import
• It is defined as a def but not and instance, meaning you need to declare the instance locally
• Someone hasn't added it to Mathlib yet
• It is mathematically incorrect

[Kevin Buzzard]

Re imports: No, it might mean that what you want isn't there at all. For example if you try to apply a theorem about groups to the natural numbers then you'll fail to synthesise the fact that they're a group no matter what you import

[W.P. McNeill]

And as far as Lean in concerned, something is mathematically incorrect if I haven't pulled in the import that tells it that it is correct. That makes sense.

[Kevin Buzzard]

No I'm not saying that, I'm saying that if Lean's typeclass inference system can't find a claim then this might be because it's not imported and it might be because it's not true.

[W.P. McNeill]

I should have been more precise. If I get "failed to synthesize" for a statement that I'm certain is mathematically correct, one explanation is that it is mathematically correct, but Lean doesn't know that it is because I haven't done the import that allows Lean to know this.

[W.P. McNeill]

Regardless, a while ago an AI told me to start with import Mathlib and I forgot. Thanks for reminding me. That's got me unstuck.

[Aaron Liu]

W.P. McNeill said:

I should have been more precise. If I get "failed to synthesize" for a statement that I'm certain is mathematically correct, one explanation is that it is mathematically correct, but Lean doesn't know that it is because I haven't done the import that allows Lean to know this.

Another explanation is that it is not mathematically correct because the definitions don't mean what you think they mean