## 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,
end,
conv at h
begin
to_rhs,
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_self,
end,
conv at h
begin
to_rhs,