# Zulip Chat Archive

## Stream: new members

### Topic: subtract equation lemma

#### Calle Sönne (Feb 25 2019 at 14:42):

I have a goal ` a = b `

and a hypothesis ``c = d `

is there a lemma that gives `a - c = b - d `

? Only way I see how to do it without the lemma is to subtract c from a = b, then use conv to rw c on rhs, but this is quite tedious.

#### Calle Sönne (Feb 25 2019 at 14:42):

I am in some ring if that is relevant

#### Kenny Lau (Feb 25 2019 at 14:43):

`congr (congr_arg (-) (hab : a = b)) (hcd : c = d)`

#### Kenny Lau (Feb 25 2019 at 14:43):

I once tried to get it to mathlib but people didn't like it

#### Kenny Lau (Feb 25 2019 at 14:44):

or you can just `have a - c = b - d, by rw [hab, hcd]`

#### Patrick Massot (Feb 25 2019 at 14:44):

I think that actually we should have more tactics like that, at least for teaching purposes

#### Gabriel Ebner (Feb 25 2019 at 15:01):

If you already have `a - c = b - d`

as a goal, then you can apply the `congr`

tactic which produces `a=b`

and `c=d`

as subgoals (there's also `congr'`

):

example (a b c d : ℕ) (h1 : a = b) (h2 : c = d) := show a - c = b - d, by congr; assumption

#### Calle Sönne (Feb 25 2019 at 16:06):

I have this goal: ` 0 = finset.sum (finset.range n) (λ (x : ℕ), digit b r x * ↑b ^ (n - x) - digit b r x * ↑b ^ (n - 1 - x + 1)) `

Im having trouble proving this, as the subtraction lemma I need require `x ≤ n`

which is only true in the finset.range n, can I "enter" the sum somehow and prove it there, given hypothesis `x ≤ n`

or similar .

#### Calle Sönne (Feb 25 2019 at 16:07):

the lemma is, nat.add_sub_assoc

#### Calle Sönne (Feb 25 2019 at 16:09):

The closest I have gotten is here:

0 = finset.sum (finset.range (1 + n)) (λ (x : ℕ), digit b r x * ↑b ^ (1 + n - x) + -(digit b r x * ↑b ^ (1 + (n - x))))

which is what requires nat.add_sub_assoc

#### Kenny Lau (Feb 25 2019 at 16:10):

finset.sum_eq_zero : ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : add_comm_monoid β] [_inst_2 : add_comm_monoid β] {f : α → β} {s : finset α}, (∀ (x : α), x ∈ s → f x = 0) → finset.sum s f = 0

#### Patrick Massot (Feb 25 2019 at 16:11):

You could use https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L124 if you were using my bigop proto-library. I don't know about finset

#### Calle Sönne (Feb 25 2019 at 16:11):

Thanks :)

#### Scott Morrison (Feb 25 2019 at 21:12):

We really need a mode in `conv`

to enter a sum (whether finset or bigop), automatically gaining the hypothesis saying that you are in the domain.

#### Patrick Massot (Feb 25 2019 at 21:13):

That would be really cool

Last updated: May 08 2021 at 05:14 UTC