Splitting a `Std.Range` / Unfold `∈` in propositions

Stream: Is there code for X?

[Ayhon]

If I have i ∈ r with i: Nat and r: Std.Range, and i < n, is there a way to derive i ∈ {r with stop := n}? I've tried to do so myself manually, but I run into trouble trying to unfold ∈. Not sure which of these two should be easier.

[Bjørn Kjos-Hanssen]

Use show, once you look up the definition of mem

import Mathlib

example (i : Nat) (r : Std.Range) (h : i < n) (g : i ∈ r) : i ∈ {r with stop := n} := by
  show r.start ≤ i ∧ i < n
  constructor
  exact Membership.mem.lower g
  exact h

[Ayhon]

Thanks! This ended up working. I'm curious why unfolding it didn't work though. What I mean is, if I use unfold Membership.mem, I get the following goal:

i m : ℕ
r : Std.Range
i_in_r : i ∈ r
i_lt_m : i < m
⊢ Std.instMembershipNatRange.1 i { start := r.start, stop := m, step := r.step }

I would expect it to fill in with the definition of Std.instMembershipNatRange.mem, not this.

[Bjørn Kjos-Hanssen]

You can do a second unfold, this time of Std.instMembershipNatRange
The .1 is actually equal to .mem here.