Questions on decreasing_by

Stream: lean4

[Ian Jauslin]

Hello! I am struggling a bit with using decreasing_by in an inductive definition. What I'm actually using this for is a bit long to write out, so let me illustrate my problem in a simpler example. If I try to do

import Mathlib.Data.Nat.Basic

def is_big (n : ℕ) :=
  match n with
  | 0 => false
  | 1 => true
  | Nat.succ n => ∃ i : ℕ, i<n ∧ is_big i
  termination_by _ => n
  decreasing_by
    simp_wf

I get a few goals, but the condition i<n is not in the hypotheses (so the goals are unprovable). How can I get i<n in the hypotheses available after decreasing_by?

Also, is match what I want to use here?

[Mario Carneiro]

you should be able to use \exists h : i < n, is_big i instead of i<n ∧ is_big i

[Ian Jauslin]

Yes, wonderful. Thank you, that works!