I want to learn a quick programming process

Stream: general

[Mason McBride]

Screenshot-2023-11-07-at-7.48.42-PM.png
What is the best way for me as a recreational lean user to read this in a textbook and convert it into lean and try to prove it in like under 20 seconds total? Anyone have a really efficient process to do this?

[Mario Carneiro]

you would have difficulty solving such an exercise in 20 seconds on paper

[Mario Carneiro]

most of the work here would be in defining what the star and bang operators there are

[Mario Carneiro]

and writing down the theorems

[Mario Carneiro]

depending on what the definitions say the proof could be very easy (e.g. rfl or by simp) or unboundedly hard (probably not too hard or else it wouldn't be phrased as an exercise like this)

[Mason McBride]

• and _* are just the image and preimage operation on a function shouldn't they be easily reachable in mathlib? and the only other operations are compostion and the identity

[Mario Carneiro]

in that case the easy solution is by exact? because this theorem already exists

[Mason McBride]

I'm asking if you know how to query mathlib for these properties in under 20 seconds to fully describe the exercise

[Mario Carneiro]

by exact?

[Mario Carneiro]

you write that and in less than 20 seconds it will suggest the relevant theorem from the library

[Mario Carneiro]

(assuming it exists, of course)

[Mason McBride]

Thank you, what is the syntax using mathlib to write the theorem statement the image of f^-1 is equal to the the inverse of the image of f?

[Mason McBride]

like what are you importing as a programmer? are you opening any namespaces?

[Mario Carneiro]

no namespaces needed

[Mario Carneiro]

here's the preimage statement:

import Mathlib.Tactic

example {X Y Z} (f : X → Y) (g : Y → Z) (s : Set Z) :
    (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s) := by exact? -- Try this: exact rfl

[Mario Carneiro]

if you wanted to write it without the set s like in the exercise you would need to use it without the notation, referring to its name Set.preimage or opening Set first:

import Mathlib.Tactic

open Set
example {X Y Z} (f : X → Y) (g : Y → Z) :
    preimage (g ∘ f) = preimage f ∘ preimage g := by exact? -- Try this: exact rfl

[Mario Carneiro]

for forward image it's not just rfl, but there is still a theorem for it:

import Mathlib.Tactic

example {X Y Z} (f : X → Y) (g : Y → Z) (s : Set X) :
    (g ∘ f) '' s = g '' (f '' s) := by exact? -- Try this: exact image_comp g f s

unfortunately this one doesn't come in unapplied form in the library so if you wanted that you would have to prove it yourself

[Mason McBride]

Awesome

[Yury G. Kudryashov]

For future questions: posting a screenshot of a lemma without providing definitions is not very helpful. Also, you can do simple stuff in 20 seconds but it takes much more time to learn how to do it in 20 seconds.

[Mario Carneiro]

yes, learning how to write these statements is going to be by far the slowest part of the work

[Mario Carneiro]

I can do it because I know the library well but it will take you quite a bit more than 20 seconds if you aren't familiar with the library, and by exact? only helps with the proofs, not the statements

[Mario Carneiro]

Potentially moogle could be helpful to this end

[Mason McBride]

but how does exact rfl help me either? what lemmas are applying?

[Mario Carneiro]

It's applying the rfl theorem

[Mario Carneiro]

which is another way to say that lean believes both sides to be equal by definition so reflexivity is a proof of the goal

[Mario Carneiro]

this is because if you unfold the definition of composition and preimage you realize both expressions are denoting the set {x | g (f x) ∈ s}

[Mario Carneiro]

there is actually a theorem docs#Set.preimage_comp which asserts this, but exact? optimistically tries rfl first because it proves quite a lot of things that you wouldn't expect at first

[Mason McBride]

preimage_comp uses rfl as proof haha