# Zulip Chat Archive

## Stream: new members

### Topic: Practicing writing proofs

#### Adomas Baliuka (Sep 03 2023 at 18:02):

I wrote a proof that subtracting two sums over `range`

s equals sum over the difference of the ranges. The proof took me a long time and seems extremely ugly. I'm hoping to learn a lot by having someone look at it for 3 seconds and say how to do it in two lines. (Please let me know in case such a question is discouraged here)

```
lemma bigsum_minus_bigsum (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n) , f (h + n) := by
induction m generalizing n with
| zero =>
have nz : n = 0 := by linarith
simp [*]
| succ m ih =>
by_cases le : n ≤ m
· rw [minus_succ_eq_succ_minus]
repeat rw [Finset.sum_range_succ]
rw [←ih]
have minsimp : m - n + n = m := by
apply tsub_add_cancel_of_le
linarith
rw [minsimp]
have kk : ∑ x in range m, f x = ∑ k in range m, f k := by simp
rw [kk]
have mycomm (a b c : ℝ) : a + b - c = a - c + b := by ring
simp [mycomm]
exact le
exact le
· have eeq : n = m + 1 := by linarith
simp [*]
```

#### Moritz Firsching (Sep 03 2023 at 18:24):

could be made shorter, but this works:

```
lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
have := Finset.sum_range_add_sub_sum_range (fun x => f x) n (m - n)
rw [add_sub_of_le mlen] at this
rw [this]
simp only [add_comm]
```

[edited: changed `covert`

to `simp only [add_comm]`

]

#### Adomas Baliuka (Sep 03 2023 at 18:30):

Wow, thanks! It says "expecting term". Is there something missing after `convert`

? Did you know about `sum_range_add_sub_sum_range`

or did you find it by some method I could learn?

#### Yaël Dillies (Sep 03 2023 at 18:33):

Here's a non-cheating proof, using only lemmas simpler than the one you're trying to prove:

```
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic
open Finset
open scoped BigOperators
lemma addRightEmbedding_eq_addLeftEmbedding {G : Type*} [AddCancelCommMonoid G] (g : G) :
addRightEmbedding g = addLeftEmbedding g := by ext; exact add_comm _ _
lemma bigsum_minus_bigsum (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n) , f (h + n) := by
simp_rw [sub_eq_iff_eq_add, ←addRightEmbedding_apply n, ←sum_map]
rw [←sum_union, union_comm]
· congr
rw [addRightEmbedding_eq_addLeftEmbedding]
convert range_add_eq_union _ _
rw [add_tsub_cancel_of_le mlen]
· simp [disjoint_left]
```

#### Yaël Dillies (Sep 03 2023 at 18:35):

Of course the better way is to use the existing lemma `sum_range_add_sub_sum_range `

, which you could have found by looking for `Finsetsumrangerange`

or `Finsetsumrangesub`

in the docs: you know each part should appear in the name somewhere, and you can try a few permutations out (but typically `sum`

will probably come before `range`

).

#### Moritz Firsching (Sep 03 2023 at 18:39):

ab said:

Wow, thanks! It says "expecting term". Is there something missing after

`convert`

? Did you know about`sum_range_add_sub_sum_range`

or did you find it by some method I could learn?

Yes, there was something missing, I changed the original message...

#### Adomas Baliuka (Sep 03 2023 at 19:36):

@Yaël Dillies If you don't mind me asking, how did you think of using these embeddings? Is that a normal technique in some circumstances? It seems very weird and roundabout somehow. You build these embedding objects and then coerce them to functions? (Is there a way to list coercions? I know about `#synth`

but there I need to know input and output type. Is there a way to list instances and filter just by input or output?)

#### Yaël Dillies (Sep 03 2023 at 19:41):

My hand was forced by the way docs#Finset.range_add_eq_union was written. To be quite honest, I would have preferred a lemma of the form `range a = range b ∪ (range (b - a)).map (addLeftEmbedding a)`

.

The reason we use those embeddings is because we want to use docs#Finset.map instead of docs#Finset.image. This (somewhat rare pattern) is useful because it lets us carry around the proof of injectivity (or in the case of docs#Finset.sup' nonemptiness, or `i ∉ s`

for docs#Finset.cons, etc...) and spares us a few proof obligations. Typically, I used docs#Finset.sum_map which doesn't require me (re)proving that the function is injective.

#### Moritz Firsching (Sep 03 2023 at 20:19):

```
lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
have := Finset.sum_range_add_sub_sum_range (fun x => f x) n (m - n)
simp only [add_comm]
convert Finset.sum_range_add_sub_sum_range _ _ _
exact (add_sub_of_le mlen).symm
```

is better than what I wrote before.

I think @ab is asking about how to go from a name "`Finsetsumrangesub`

" to the name of the theorem and one answer here is to use the search of https://leanprover-community.github.io/mathlib4_docs/. If you already know where to look for approximately, then typing `Finset.sum`

and pressing Ctrl-space will show suggestions.

for the last exact, you can simply type `exact?`

and it should find the ` (add_sub_of_le mlen).symm`

part

#### Adomas Baliuka (Sep 04 2023 at 15:11):

@Moritz Firsching Why is this better? It has the same number of lines. I'm trying to understand what kind of proofs and style are considered "good".

#### Ruben Van de Velde (Sep 04 2023 at 15:18):

The `have := ..`

is superfluous in the latest proof

#### Ruben Van de Velde (Sep 04 2023 at 15:22):

I'm not sure I agree it's better, in any case, since the `simp only [add_comm]`

is still somewhat unfortunate. If you want to use `convert`

(which means "I've *nearly* got the result I need, please show me where it differs from the current goal"), maybe this is nicer:

```
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic
open BigOperators Finset Nat
lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
convert Finset.sum_range_add_sub_sum_range _ _ _ using 3
· rw [add_sub_of_le mlen]
· exact add_comm _ _
```

#### Ruben Van de Velde (Sep 04 2023 at 15:27):

Or you could do:

```
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic
open BigOperators Finset Nat
lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) :=
calc
_ = ∑ k in range (n + (m - n)), f k - ∑ k in range n, f k := by rw [add_sub_of_le mlen]
_ = ∑ k in range (m - n), f (n + k) := Finset.sum_range_add_sub_sum_range ..
-- Choose one of the following two lines
-- _ = _ := by simp_rw [add_comm]
-- _ = _ := Finset.sum_congr rfl fun _ _ => by rw [add_comm]
```

Not sure any of those are necessarily better or worse than the other alternatives

Last updated: Dec 20 2023 at 11:08 UTC