basic lean commands

Stream: new members

[Pedro Castilho]

hi, am trying to get more familiar with ⟨⟩ operator, I know it can be used for "and.intro", but I can't get the reason of the x in ⟨x, h6, h5⟩ to show y ∈ f '' (A ∪ B), why isn't ⟨h6, h5⟩ enough?

have h4 : x ∈ A, from h.left,
        have h5 : f x = y, from h.right,
        have h6 : x ∈ A ∪ B, from or.inl h4,
        show y ∈ f '' (A ∪ B), from ⟨x, h6, h5⟩)

[Yury G. Kudryashov]

y ∈ f '' (A ∪ B) unfolds to ∃ x, x ∈ A ∧ f x = y

[Yury G. Kudryashov]

So, ⟨x, h6, h5⟩ unfolds to something like Exists.intro x (and.intro h6 h5)

[Pedro Castilho]

ah, that makes sense, thx @Yury G. Kudryashov

[Pedro Castilho]

do you have any references to the ⟨⟩ syntax? it looks really nice in proofs and I wanted to get a better feel for it

[Yury G. Kudryashov]

If Lean knows the expected type of an expression and this type has exactly one constructor, then ⟨...⟩ applies this constructor.

[Pedro Castilho]

that's really cool thanks

[Yury G. Kudryashov]

And you can write ⟨a, ⟨b, c⟩⟩ as ⟨a, b, c⟩. Note that you can't write ⟨⟨a, b⟩, c⟩ as ⟨a, b, c⟩.

[Bryan Gin-ge Chen]

I linked to a few mentions of the angle bracket notation in #TPiL in this thread.

[Pedro Castilho]

oh, that's really helpful @Bryan Gin-ge Chen

[Pedro Castilho]

i have been in leans Zulip community for a couple of weeks and I have to say that its a really great one, you guys are super helpful

[Pedro Castilho]

thx again for all the help

[Pedro Castilho]

and I hope soon enough I can help other around here hehehe

[Bryan Gin-ge Chen]

Happy to have you around, Pedro!

[Eduardo Vianna]

I'm having doubts when prooving an example image.png
I used the "assume x" hoping to do a universal introduction (to prove ∀ (x : B), v1 x = v2 x and consequently v1 = v2), but it is not working and I can't figure why!
Here's the type mismatch notification lean gives me at this marked "show":
"type mismatch at application
(λ (this : ∀ (x : B), v1 x = v2 x), this) h
term
h
has type
v1 x = v2 x
but is expected to have type
∀ (x : B), v1 x = v2 x"

[Mario Carneiro]

#backticks

[Bryan Gin-ge Chen]

You'll need to use function extensionality, which is funext.

[Mario Carneiro]

brian is right, you need funext $ assume x, ... instead of assume x, ...

[Bryan Gin-ge Chen]

Here's a working proof:

open function

example (A B : Type) (u : A → B) (v1 : B → A) (v2 : B → A)
  (h1 : left_inverse v1 u) (h2 : right_inverse v2 u) : v1 = v2 :=
funext $ assume x,
  have h : v1 x = v2 x, from
  calc
    v1 x = v1 (u (v2 x)) : by rw h2
    ... = v2 x : by rw h1,
  show v1 x = v2 x, from h

By the way, it's much easier for us to help if you copy+paste a #mwe; screenshots are hard to work off of.