How to get the proof of not equal to previous terms in match

Stream: new members

[ShatteredLead]

  def g (x : ℕ) : ℕ :=
    match x with
      | 0 => 1
      | 1 => -- there's something requires x ≠ 0, and how can we prove it?

[Edward van de Meent]

do you mean match x with?

[ShatteredLead]

Edward van de Meent said:

do you mean match x with?

Yeah, sorry for the typo

[Edward van de Meent]

i think easiest way would be to use if h:x=0 then default else [insert term using h]

[Daniel Weber]

You can also do

import Mathlib

def g (x : ℕ) : ℕ :=
  match h : x with
    | 0 => 1
    | 1 =>
      -- h : x = 1
      sorry
    | _ => sorry

[Edward van de Meent]

ooh, i didn't know about that one, that does look better!

[ShatteredLead]

appreciate it!

[ShatteredLead]

Daniel Weber said:

You can also do

import Mathlib

def g (x : ℕ) : ℕ :=
  match h : x with
    | 0 => 1
    | 1 =>
      -- h : x = 1
      sorry
    | _ => sorry

  def g (x : ℕ) : ℕ :=
    match h: x with
      | 0 => -- ...
      | 1 => -- ...
      | 2 => -- ...
      | k => -- how to get x > 2 here?

But in this situation, it seems we only can know h : x = k

[Yaël Dillies]

def g (x : ℕ) : ℕ :=
  match h : x with
  | 0 => _
  | 1 => _
  | 2 => _
  | k + 3 => _