obtain tactic vs have

Stream: new members

[Kevin Cheung]

There is the following example in Mathematics in Lean in Section 3.2:

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnHasUb (f : ℝ → ℝ) :=
  ∃ a, FnUb f a

theorem fnUb_add {f g : ℝ → ℝ} {a b : ℝ} (hfa : FnUb f a) (hgb : FnUb g b) :
    FnUb (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  obtain ⟨a, ubfa⟩ := ubf
  obtain ⟨b, ubgb⟩ := ubg
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

Replacing the two obtains in the example also works. Other than that obtain removes the original hypothesis from the context, how else could have and obtain differ? I tried to construct an example where one could deconstruct with obtain but not with have. So far no success. Help much appreciated.

[Ruben Van de Velde]

It has a few more bells and whistles:

import Mathlib

example : True := by
  obtain ⟨x, rfl⟩ : ∃ x, x = 1 := ⟨_, rfl⟩
  obtain h | h : True ∨ ¬ True := em True
  all_goals trivial

[Kevin Cheung]

Wow. Thanks. I wouldn't have come up with these.

[Mark Fischer]

"The obtain tactic is a combination of have and rcases"

Here's the docs on rcases. The recursive pattern matching with rcases can sometimes save you a lot of boilerplate.