Can't `rw if_pos` in `let`

Stream: new members

[Marcus Rossel]

Ok, I've got another one I don't know how to fix:

def ports : Type* := list (option empty)
instance : has_append ports := ⟨list.has_append.append⟩

def merge (first last : ports) : ports :=
    let p' := last.zip_with (<|>) first in
    if first.length ≤ last.length then p' else p' ++ list.repeat none (first.length - last.length)

example (p : ports) : merge p (list.repeat none p.length) = p :=
begin
  unfold merge,
  have h : list.length p ≤ list.length (list.repeat (none : option empty) (list.length p)), from sorry,
  rw if_pos h,

end

I would like to apply rw if_pos h, but get an error, even though I've literally copy-pasted the hypothesis h out of the goal.
How can I solve this?

[Patrick Massot]

The main trick is is to read the webpage #mwe.

[Marcus Rossel]

Patrick Massot said:

The main trick is is to read the webpage #mwe.

Haha sorry, I've updated the example above.

[Patrick Massot]

Using let like this is asking for trouble.

[Marcus Rossel]

Patrick Massot said:

Using let like this is asking for trouble.

I've heard this before. What is the right way to use let then, and how can I circumvent it in this example?

[Patrick Massot]

What about

def merge (first last : ports) : ports :=
    (last.zip_with (<|>) first) ++
    (if first.length ≤ last.length then list.nil else list.repeat none (first.length - last.length))

[Marcus Rossel]

Patrick Massot said:

What about

def merge (first last : ports) : ports :=
    (last.zip_with (<|>) first) ++
    (if first.length ≤ last.length then list.nil else list.repeat none (first.length - last.length))

Ah yes, :face_palm:🏼‍♀️ Thanks :D