## Stream: new members

### Topic: basic lean commands

#### Pedro Castilho (Nov 05 2020 at 03:17):

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 (Nov 05 2020 at 03:24):

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

#### Yury G. Kudryashov (Nov 05 2020 at 03:25):

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

#### Pedro Castilho (Nov 05 2020 at 03:27):

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

#### Pedro Castilho (Nov 05 2020 at 03:29):

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 (Nov 05 2020 at 03:30):

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

#### Pedro Castilho (Nov 05 2020 at 03:31):

that's really cool thanks

#### Yury G. Kudryashov (Nov 05 2020 at 03:31):

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 (Nov 05 2020 at 03:34):

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

#### Pedro Castilho (Nov 05 2020 at 03:40):

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

#### Pedro Castilho (Nov 05 2020 at 03:42):

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 (Nov 05 2020 at 03:42):

thx again for all the help

#### Pedro Castilho (Nov 05 2020 at 03:44):

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

#### Bryan Gin-ge Chen (Nov 05 2020 at 03:44):

Happy to have you around, Pedro!

#### Eduardo Vianna (Nov 06 2020 at 01:06):

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"

#backticks

#### Bryan Gin-ge Chen (Nov 06 2020 at 01:15):

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

brian is right, you need funext $assume x, ... instead of assume x, ... #### Bryan Gin-ge Chen (Nov 06 2020 at 01:19): 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.

Last updated: May 16 2021 at 20:13 UTC