Decidable version of monotone_lt

Stream: new members

[Julia Scheaffer]

I am trying to figure out how to prove this

import Mathlib
def f (i : Nat) : Nat -> Bool := (i < ·)

example {i : Nat} : Monotone (f i) := by
  unfold f
  exact monotone_lt -- doesn't work because of decide i think

Is it possible to use docs#monotone_lt for this or do I need to use another method?

[Aaron Liu]

import Mathlib
def f (i : Nat) : Nat -> Bool := (i < ·)

example {i : Nat} : Monotone (f i) := by
  intro a b hab
  simp only [f, Bool.le_iff_imp, decide_eq_true_eq]
  order

[Julia Scheaffer]

Thank you :smile:

[Kenny Lau]

@Julia Scheaffer it's because the theorem you want to use monotone_lt is about a function to Prop, whereas the theorem you want to provev is about a function to Bool, and Prop and Bool are very different even though you might have taught a mental model where they are the "same"

[Julia Scheaffer]

Yeah, I just wasn't sure about how to convert between them in the case that i have a decidable prop

[Julia Scheaffer]

But thanks to Aaron, I got it worked out.