by_cases in term mode definition?

Stream: new members

[ROCKY KAMEN-RUBIO]

Is there a way to do the equivalent of by_cases in term mode? Specifically, I mean check whether a given condition is met so we can call another definition/theorem that requires it, else give some other value. Here's an example

def h (a b : ℝ) (h : a ≠ b) : Prop := 1 / (a - b) > 0

def g' (a b : ℝ) : Prop :=
begin
  by_cases hab : a = b,
  {exact tt},
  exact h a b hab,
end

def g (a b : ℝ) : Prop := a = b ∨ h a b _,

[Mario Carneiro]

if hab : a = b then tt else h a b hab

[Mario Carneiro]

That's the direct translation, but in this case you can use \forall hab : a != b, h a b hab