# Zulip Chat Archive

## Stream: new members

### Topic: How do I get lamdas to apply outside of a lemma

#### Lars Ericson (Dec 24 2020 at 20:06):

I have a lemma which is defined as a particular term application which involves a lambda. If I apply the lemma, the lambda reduces. If I apply the term application, it does not. Is there a way to get the direct term application to reduce the lambda? Here is the sketch:

```
import algebra.ring.basic
import tactic
universe u
variables {α : Type u} [integral_domain α] {a b c d : α}
lemma foo : a = b + (c - d) → a + d = b + (c - d) + d := congr_arg (λ {a : α}, a + d)
#check @foo α _ a b c d
#check @congr_arg α α a (b+(c-d)) (λ {a : α}, a + d)
```

You can see the difference here:

```
lemma ex5dLR : a-b=c-d → a+d=b+c :=
begin
intro h1,
have h2 := @eq_add_of_sub_eq' α _ a b (c-d),
have h3 := h2 h1,
have h4 := @congr_arg α α a (b+(c-d)) (λ {a : α}, a + d),
have h5 := h4 h3,
have h4a := @foo α _ a b c d,
have h5a := h4a h3,
end
```

where the state is

```
α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h1 : a - b = c - d,
h2 : a - b = c - d → a = b + (c - d),
h3 : a = b + (c - d),
h4 : a = b + (c - d) → ((λ {a : α}, a + d) = λ {a : α}, a + d),
h5 : (λ {a : α}, a + d) = λ {a : α}, a + d,
h4a : a = b + (c - d) → a + d = b + (c - d) + d,
h5a : a + d = b + (c - d) + d
⊢ a + d = b + c
```

and `h5a`

is nice and `h5`

has lambdas.

#### Eric Wieser (Dec 24 2020 at 20:22):

What exactly is your question? Do you want to turn h5 into h5a, vice versa, or something else?

#### Adam Topaz (Dec 24 2020 at 20:31):

I think you should take a look at the tactic `apply_fun`

, it's a `fun`

way to solve this example :wink:

#### Eric Wieser (Dec 24 2020 at 20:42):

Or is your question how to convert `(λ a, f a) x`

to `f x`

? If so, the answer is either "they're already equal by `rfl`

", or tactic#delta

#### Lars Ericson (Dec 24 2020 at 21:01):

I am trying to avoid introducing extraneous lemmas, which is against the style guide. I wasn't able to figure out how to use `apply_fun`

or `delta`

in this example to avoid adding a few lemmas:

```
import algebra.ring.basic
import tactic
import tactic.apply_fun
universe u
variables {α : Type u} [integral_domain α] {a b c d : α}
lemma foo : a = b + (c - d) → a + d = b + (c - d) + d := congr_arg (λ {a : α}, a + d)
lemma bar : b + (c - d) + d = b + c :=
begin
ring,
end
lemma ex5dLR : a-b=c-d → a+d=b+c :=
begin
intro h1,
have h2 := @eq_add_of_sub_eq' α _ a b (c-d),
have h3 := h2 h1,
have h4 := @foo α _ a b c d,
have h5 := h4 h3,
conv at h5
begin
to_rhs,
rw bar,
end,
exact h5,
end
```

#### Adam Topaz (Dec 24 2020 at 21:05):

Here's an example to get you started:

```
import algebra
import tactic.apply_fun
example {α : Type*} [integral_domain α] (a b c : α) : a - c = b - c → a = b :=
begin
intro h,
apply_fun (λ t, t + c) at h,
simp at h,
assumption
end
```

#### Lars Ericson (Dec 24 2020 at 21:29):

Thanks. In this example:

```
example : a+d=b+c → a-b=c-d :=
begin
intro h,
apply_fun (λ t, t-b-d) at h,
simp at h,
end
```

after the `apply_fun`

I have

```
h: a + d - b - d = b + c - b - d
```

and I want it to simplify to

```
h: a - b = c - d
```

Instead the `simp at h`

gives

```
h: a + d - b = c
```

If instead I got into `conv`

mode and just try to simplify just the left hand side of `h`

:

```
example : a+d=b+c → a-b=c-d :=
begin
intro h,
apply_fun (λ t, t-b-d) at h,
conv at h
begin
to_lhs,
simp,
end
end
```

after the `to_lhs`

my goal state is

```
1 goal
α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h : a + d - b - d = b + c - b - d
| a + d - b - d
```

after the `simp`

but before exiting the `conv`

block it becomes

```
state:
α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h : a + d - b - d = b + c - b - d
⊢ a + d - b - d = ?m_1
```

and out of the `conv`

block there is no change on `h`

:

```
α: Type u
_inst_1: integral_domain α
abcd: α
h: a + d - b - d = b + c - b - d
⊢ a - b = c - d
```

How do I apply `simp`

to just left hand side or right hand side? I tried `simp at h.left`

but that doesn't parse.

#### Eric Wieser (Dec 24 2020 at 21:54):

You can always use `have`

to set an intermediate goal of the form you want and have simp solve that goal

#### Lars Ericson (Dec 25 2020 at 00:54):

DONE. The lesson learned is that a covering set of lemmas for common algebraic manipulations is in `algebra.group.basic`

:

```
import algebra.ring.basic
import tactic
import tactic.apply_fun
universe u
variables {α : Type u} [integral_domain α] {a b c d : α}
lemma ex5d : a-b=c-d ↔ a+d=b+c :=
begin
split,
{
intro h,
apply_fun (λ t, t+b+d) at h,
conv at h
begin
to_lhs,
rw sub_add_cancel,
end,
conv at h
begin
to_rhs,
rw sub_add_eq_add_sub,
rw sub_add,
rw sub_self,
rw sub_zero,
end,
have swap := add_comm c b,
rw swap at h,
assumption,
},
{
intro h,
apply_fun (λ t, t-b-d) at h,
conv at h
begin
to_lhs,
rw ← sub_add_eq_add_sub,
rw ← add_sub,
rw sub_self,
rw add_zero,
end,
conv at h
begin
to_rhs,
rw ← sub_add_eq_add_sub,
rw sub_self,
rw zero_add,
end,
assumption,
},
end
```

Last updated: May 13 2021 at 23:16 UTC