deriving `ℝ` as a goal state?

Stream: new members

[Chris M]

I am trying to just apply the proof monof to h using the have keyword. However, for some reason it gives me a few goal states that I don't understand. This is my code:

example :
  ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { exact monotone_const},
  have h' : f 1 ≤ f 0,
    from le_refl _,
  have h2 := (h monof),
end

This generates three goal states. The first is the one that I actually wanted:

h : ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
f : ℝ → ℝ := λ (x : ℝ), 0,
monof : monotone f,
h' : f 1 ≤ f 0,
h2 : f ?m_1 ≤ f ?m_2 → ?m_1 ≤ ?m_2
⊢ false

But it also generates these goal states that I haven't seen before. It wants me to "derive" ℝ twice...?

h : ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
f : ℝ → ℝ := λ (x : ℝ), 0,
monof : monotone f,
h' : f 1 ≤ f 0
⊢ ℝ

h : ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
f : ℝ → ℝ := λ (x : ℝ), 0,
monof : monotone f,
h' : f 1 ≤ f 0
⊢ ℝ
````

[Mario Carneiro]

Those two are ?m_1 and ?m_2 that you can see in the type of h2 in the first goal

[Mario Carneiro]

You can mostly ignore them because they usually go away when you finish the proof

[Mario Carneiro]

In this case, you presumably want to derive 1 <= 0 using h', so you should finish the application and write have h2 := h monof h', and then those side goals will disappear

[Eric Wieser]

Something which I brought up in lftcm - it would be great if m_1 could be used as a heading for it's associated goal in the lean goal state window

[Kevin Buzzard]

I'm not sure that the goal knows it's called ?m_1 in another goal

[Mario Carneiro]

Unfortunately it doesn't work because the metavariables are given new names every time they get printed

[Mario Carneiro]

I don't know how hard it would be to change the pretty printer so that metavariable numbering can be shared across multiple goals