subtract equation lemma

Stream: new members

[Calle Sönne]

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]

I am in some ring if that is relevant

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Patrick Massot]

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

[Gabriel Ebner]

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]

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]

the lemma is, nat.add_sub_assoc

[Calle Sönne]

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]

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]

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]

Thanks :)

[Scott Morrison]

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]

That would be really cool