## 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: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))))


#### 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

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