theorem with pfun and part

Stream: general

[David Richey]

I am struggling to prove the following:

import data.pfun
lemma foo {α β} {f : α →. β} {x y} (h : f x = part.some y) : ∃ha, f.fn x ha = y :=
begin
  have h1 : f.dom x, -- kind of blindly applied `suggest` to find this, might not be the best...
    refine set.mem_preimage.mpr _,
    exact set.mem_of_eq_of_mem h trivial,

  apply exists.intro,
    -- ⊢ f.fn x ?m_1 = y
    sorry,
    apply h1,
end

I think the core components I need to use to fix that sorry are pfun.fn_apply and part.some_get, but I'm failing to come up with anything. Does anyone have any suggestions?

[Ruben Van de Velde]

Your code doesn't compile for me - do you have a #mwe?

[David Richey]

that's strange, it does compile for me

[David Richey]

oh, it is missing the import data.pfun

[Ruben Van de Velde]

Ah, that's better. apply exists.intro, is pretty strange; maybe use h1?

[David Richey]

ah ok, that saves me from the second subgoal, but I think I'm mostly in the same place. To expand on what I've tried so far... I _want_ to write

use h1,
rewrite pfun.fn_apply,
rewrite h,

but this gives

rewrite tactic failed, motive is not type correct
  λ (_a : part β), (f x).get h1 = y = (_a.get h1 = y)

I'm not sure how to tell what doesn't type check here

[Kyle Miller]

There are some dependencies in there, but simp is able to do the rewrite.

[Kyle Miller]

In fact,

lemma foo {α β} {f : α →. β} {x y} (h : f x = part.some y) : ∃ha, f.fn x ha = y :=
⟨set.mem_preimage.mpr (set.mem_of_eq_of_mem h trivial), by simp [h]⟩

[David Richey]

oh! I'm afraid there's more than a few instances of unfamiliar syntax for me here haha

[Kyle Miller]

The angle brackets are equivalent to this in this case:

lemma foo {α β} {f : α →. β} {x y} (h : f x = part.some y) : ∃ha, f.fn x ha = y :=
exists.intro (set.mem_preimage.mpr (set.mem_of_eq_of_mem h trivial)) (by simp [h])

[David Richey]

if you don't mind, what would be the more verbose version in tactic mode?

[Kyle Miller]

lemma foo {α β} {f : α →. β} {x y} (h : f x = part.some y) : ∃ha, f.fn x ha = y :=
begin
  use set.mem_preimage.mpr (set.mem_of_eq_of_mem h trivial),
  simp [h],
end

[David Richey]

thank you very much! I think from here I can investigate the square bracket notation for simp