Proving `mem_approx` for functions involving `ofNat`

[adomasbaliuka]

How should one prove mem_approx_f below?

I don't know how to prove the sorry and also don't know how one might generalize mem_approx_ofNat to work for numbers besides 2.

import Interval

def Interval.f (x : Interval) : Interval := x / 2

noncomputable def Real.f (x : ℝ) : ℝ := x / 2

@[mono] lemma mem_approx_ofNat :
  (n : ℝ) ∈ approx (OfNat.ofNat 2 : Interval) := by
  sorry

@[mono] lemma mem_approx_f (ix : Interval) (x : ℝ) (is_approx_x : x ∈ approx ix) :
    x.f ∈ approx ix.f := by
  simp [Interval.f, Real.f]
  mono

With naive approach of adding

@[mono] lemma mem_approx_ofNat' {n : ℕ} [OfNat Interval n]:
  (n : ℝ) ∈ approx (OfNat.ofNat n : Interval) := by
  sorry

@[mono] lemma mem_approx_f (ix : Interval) (x : ℝ) (is_approx_x : x ∈ approx ix) :
    x.f ∈ approx ix.f := by
  simp [Interval.f, Real.f]
  mono
  exact mem_approx_ofNat'

mono does not pick up on it.

[girving]

Sorry for delay! I've updated to recent Mathlib now, and also ported my mono machinery over to a much cleaner custom approx tactic built on Aesop. The new version of your code is:

import Interval

def Interval.f (x : Interval) : Interval := x / 2

noncomputable def Real.f (x : ℝ) : ℝ := x / 2

@[mono] lemma mem_approx_f (ix : Interval) (x : ℝ) (m : x ∈ approx ix) :
    x.f ∈ approx ix.f := by
  simp only [Real.f, Interval.f]
  approx

[girving]

Unfortunately all the OfNat related lemmas have to be carefully marked with no_index due to https://github.com/leanprover/lean4/issues/2867, but this should be all done now.

[adomasbaliuka]

That works great, thanks!