# Zulip Chat Archive

## Stream: new members

### Topic: applying a hypothesis several times

#### Jakob Scholbach (Jan 28 2021 at 18:58):

I am working through §2 of the mathematics in lean tutorial. I have tried this

```
import data.real.basic
variables a b c : ℝ
-- BEGIN
example : max a b = max b a :=
begin
apply le_antisymm,
have h : ∀ x y, max x y ≤ max y x,
{
intros x y,
apply max_le,
apply le_max_right,
apply le_max_left,
},
apply h,
apply h
end
```

but this does not work (the last apply h does not work). I see how to fix it by replacing the proof by

```
begin
have h : ∀ x y, max x y ≤ max y x,
{
intros x y,
apply max_le,
apply le_max_right,
apply le_max_left,
},
apply le_antisymm,
apply h,
apply h
end
```

However, I don't understand why the first does not work, while the second does.

Can someone explain that?

Also, is there a way to say "have h ...", prove it, and use this established fact twice?

#### Mario Carneiro (Jan 28 2021 at 19:00):

The `have`

only exists in the first goal when you write it after `le_antisymm`

#### Mario Carneiro (Jan 28 2021 at 19:01):

the solution is to do the `have`

before both of your goals, as in the second version. That also answers your second question: yes there is a way, you just did it

#### Jakob Scholbach (Jan 28 2021 at 19:08):

What is the overarching rationale / logic behind this dependence of ordering? (Me old-fashioned guy thinking: in a paper proof it would not matter...)

#### Reid Barton (Jan 28 2021 at 19:10):

It "obviously" doesn't matter where you prove `h`

here because the hypotheses are the same for both goals, but if you did something like a case analysis, and you prove a claim in one case, you can't automatically apply it in the other case as well

#### Mario Carneiro (Jan 28 2021 at 20:52):

Also, syntactically there is a scoping consideration; in the first version, after the have you have basically generated a term like

```
le_antisymm ((\lam h : ∀ x y, max x y ≤ max y x, _) <proof>) _
```

where the two underscores are the two subgoals, and `h`

is only in scope in the first one (the first subgoal), whereas the second proof is

```
(\lam h : ∀ x y, max x y ≤ max y x, le_antisymm _ _) <proof>
```

and now `h`

is in scope for both goals.

#### Johan Commelin (Jan 28 2021 at 21:18):

@Jakob Scholbach another example: suppose you do induction, and you get two goals: the `0`

case and the `n+1`

case. The you might be able to prove `have h : bla`

in the `0`

case, but the same proof might not work (or even make sense) in the other case.

#### Kevin Buzzard (Jan 28 2021 at 21:27):

After `apply le_antisymm,`

you have two goals, and are now operating in two completely independent universes which have no way of communicating with each other.

#### Kyle Miller (Jan 28 2021 at 22:56):

Jakob Scholbach said:

What is the overarching rationale / logic behind this dependence of ordering? (Me old-fashioned guy thinking: in a paper proof it would not matter...)

A tactic proof is a sequence of instructions to manipulate the tactic state. It's all fairly low-level -- and for a practitioner it's good if basic tactics don't have too many smarts because then you have a better chance at predicting what they will do.

In principle, someone could probably write a `remember h`

tactic to extract a hypothesis to other parallel goals, but in practice it's easy enough to just reorder things.

Regarding your example, you can apply a tactic proof to all goals simultaneously:

```
example : max a b = max b a :=
begin
apply le_antisymm,
all_goals
{ have h : ∀ x y, max x y ≤ max y x,
{ intros x y,
apply max_le,
apply le_max_right,
apply le_max_left, },
apply h, },
end
```

Last updated: May 16 2021 at 21:11 UTC