oh noes i don't know how to manipulate the arrows

Stream: new members

[Huỳnh Trần Khanh]

this problem looks somewhat tractable... until i read the formalized statement :cry: https://do.proof.in.tum.de/competitions/contest/13/tasks/2/

oh noes i can see some weird symbols and when i ctrl click on them i see weird definitions and i have absolutely no idea how to manipulate them

[Huỳnh Trần Khanh]

it seems that the proof is already in mathlib (extend_function_of_lt) but i have no idea what the theorem states

[Johan Commelin]

Do you mean the $\hookrightarrow$ arrows?

[Johan Commelin]

Those are embeddings: a function, together with a proof that it is injective.

[Huỳnh Trần Khanh]

↥, ↑ and ↪. So... ↪ is a structure that bundles a function with a proof, ↥ coerces a predicate to a type and ↑ coerces a finset to a set, and a set is a predicate. That's all I know.

[Johan Commelin]

Looks good to me

[Kevin Buzzard]

If you have a question then perhaps you should ask it explicitly rather than just throwing around a link and complaining about stuff which you don't understand but which others probably do.

[Kevin Buzzard]

I do agree that it's interesting that the second Lean version in the resources has a lot more funky arrows than the first one :-)

[Huỳnh Trần Khanh]

not a lot lol, like there are only 2 more arrows :joy:

hmm so to deal with the arrows i should just like... try to unfold them? i mean the ↥ and the ↑
this is what i got

lemma goal_injective : ∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), set.restrict h S = f := begin
  intros a b,
  rw coe_sort at b,
  rw coe at b,
  rw lift_t at b,
  --
end

[Huỳnh Trần Khanh]

like i'm really confused i don't know where to start :cry:

[Kevin Buzzard]

Yeah, unfolding is never the right thing to do basically. However it is a very good way of learning about definitional equality, I used to do it a lot. Nowadays I look at problems like this from the top down -- instead of trying to manipulate the things I'm given, I ask myself what the actual proof is that I want to formalise first.

Rather than unfolding, you might want to instead ask yourself what you want from an injective map, e.g. you might want to get the underlying map, and the proof that it's injective. Similarly you might ask what you want from a coercion from finsets to sets to types, probably you just want some dictionary which can take you from an element of one to an element of the other, for example. Unfolding won't give this (at least not easily). Here you should be using the API.

[Huỳnh Trần Khanh]

(deleted)

[Huỳnh Trần Khanh]

(deleted)