## Stream: new members

### Topic: by_cases in term mode definition?

#### ROCKY KAMEN-RUBIO (Jul 04 2020 at 19:30):

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 (Jul 04 2020 at 20:02):

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

#### Mario Carneiro (Jul 04 2020 at 20:03):

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

Last updated: May 15 2021 at 00:39 UTC