# Zulip Chat Archive

## Stream: new members

### Topic: Use of "let" in tactic mode

#### Lars Ericson (Nov 26 2020 at 21:03):

The text gives this example of using `let`

:

```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩
```

I am trying to adapt this to tactic mode. This works:

```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
exact (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
end
```

However, this does not work:

```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
exact h2,
end
```

I get this error:

```
invalid match/convoy expression, expected type is not known
state:
α : Type u_1,
p q : α → Prop,
h : ∃ (x : α), p x ∧ q x
⊢ ∃ (x : α), q x ∧ p x
```

My prior experience has been that this:

```
example foo :=
begin
have h := bar,
exact h,
end
```

is equivalent to this:

```
example foo :=
begin
exact bar,
end
```

Why does the equivalence not hold in the above case?

#### Logan Murphy (Nov 26 2020 at 21:06):

Looking at your tactic state, i think you just need to switch

```
have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
```

to

```
have h2 := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hpw, hqw⟩),
```

#### Logan Murphy (Nov 26 2020 at 21:07):

i.e. right now p and q don't match up exactly with the goal, they are swapped

#### Reid Barton (Nov 26 2020 at 21:08):

The error message sort of tells you the reason. If your goal is `foo`

and you write `exact bar`

, then Lean knows that `bar`

is supposed to have type `foo`

and it can use this to make sense of `bar`

. If you write `have h := bar`

, then Lean doesn't know what you are intending to do with `h`

and it has to make sense of `bar`

in isolation, and usually this is harder.

#### Reid Barton (Nov 26 2020 at 21:08):

If you write `have h : foo := bar`

then Lean has the same information again.

#### Lars Ericson (Nov 26 2020 at 21:12):

Thank you @Reid Barton :

```
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
have h2 : ∃ x, q x ∧ p x := (let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩),
exact h2,
end
```

#### Reid Barton (Nov 26 2020 at 21:18):

This is a very unnatural way to write the proof of course

#### Reid Barton (Nov 26 2020 at 21:18):

The (mathlib) tactic equivalent to `let`

with a pattern is `obtain`

#### Reid Barton (Nov 26 2020 at 21:20):

```
import tactic.basic
example (a : Type) (p q : a -> Prop) (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
obtain ⟨w, hpw, hqw⟩ := h,
exact ⟨w, hqw, hpw⟩,
end
```

#### Lars Ericson (Nov 26 2020 at 21:38):

@Reid Barton if I try to use `obtain ⟨w, hpw, hqw⟩ := h`

to unpack `h : ∃ (x : α), p x ∧ r`

where the current goal state is:

```
27:6: goal
α : Type u_1,
p : α → Prop,
r : Prop,
h : ∃ (x : α), p x ∧ r
⊢ r
```

in this example:

```
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end
```

a lot of errors result:

```
Display GoalDisplay Messages
27:4: error:
unknown identifier 'obtain'
27:12: error:
unknown identifier 'w'
27:15: error:
unknown identifier 'hpw'
27:20: error:
unknown identifier 'hqw'
27:25: error:
invalid 'begin-end' expression, ',' expected
27:4: error:
don't know how to synthesize placeholder
context:
α : Type u_1,
p : α → Prop,
r : Prop
⊢ Type ?
```

#### Reid Barton (Nov 26 2020 at 21:39):

Yes, it's in mathlib

#### Lars Ericson (Nov 26 2020 at 21:42):

I see tactic.interactive.obtain but I get the same error even if I open it:

```
open tactic.interactive
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end
```

If I try to use the full name of `obtain`

:

```
open tactic.interactive
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
tactic.interactive.obtain ⟨w, hpw, hqw⟩ := h,
},
sorry,
end
```

then I get this:

```
Display GoalDisplay Messages
29:31: error:
unknown identifier 'w'
29:34: error:
unknown identifier 'hpw'
29:39: error:
unknown identifier 'hqw'
29:44: error:
invalid 'begin-end' expression, ',' expected
29:4: error:
unknown identifier 'tactic.interactive'
29:22: error:
invalid field notation, type is not of the form (C ...) where C is a constant
⁇
has type
?m_1
29:4: error:
don't know how to synthesize placeholder
context:
α : Type u_1,
p : α → Prop,
r : Prop
⊢ Type ?
```

#### Reid Barton (Nov 26 2020 at 21:43):

You need to import it, not open it

#### Reid Barton (Nov 26 2020 at 21:43):

Er, import some module which exports it (basically all of mathlib)

#### Lars Ericson (Nov 26 2020 at 23:17):

@Reid Barton , switching `import`

for `open`

didn't obtain `obtain`

. It's OK, I did it without it. It turns out I can instantiate an existential with `cases`

:

```
open classical
variables (α : Type*) (p q : α → Prop)
variable r : Prop
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor,
exact px,
},
{
cases h with x pxr,
exact pxr.right,
}
},
{
intro h,
cases h with h1 h2,
cases h1 with x px,
have hpxr := and.intro px h2,
constructor,
exact hpxr,
},
end
```

#### Reid Barton (Nov 27 2020 at 00:01):

`import tactic.basic`

Last updated: May 10 2021 at 00:31 UTC