Why is le_trans not working as expected here?

Stream: new members

[JK]

I'm a bit confused why le_trans works in the following proof

import Mathlib.Data.Real.Basic

section
variable {α : Type*} [PartialOrder α]
variable (s : Set α) (x a b : α)

example (H : x ≤ a) (H': a ≤ b) : x ≤ b := by
  apply le_trans
  exact H
  exact H'

end

but not in the following one:

import Mathlib.Data.Real.Basic

section
variable {α : Type*} [PartialOrder α]
variable (s : Set α) (x a b : α)

def SetUb (s : Set α) (a : α) :=
  ∀ x, x ∈ s → x ≤ a

example (h : SetUb s a) (h' : a ≤ b) : SetUb s b := by
  intro x
  dsimp [SetUb] at h
  intro xs
  apply le_trans

[Ruben Van de Velde]

What doesn't work?

[JK]

Well, I expected le_trans to reduce the goal of proving x ≤ b to proving x ≤ a and a ≤ b but that is not what I see.

[JK]

Hmm, ok, I take it back. I was confused by the state **⊢** x ≤ ?b that appeared in the InfoView (and was different from what I observed in the previous proof), but in the end it worked ok.