# Zulip Chat Archive

## Stream: new members

### Topic: use of finset.sum_insert

#### Alex Zhang (May 27 2021 at 09:51):

```
import algebra.big_operators.basic
import data.real.basic
import set_theory.cardinal
open_locale big_operators
lemma sum_of_squares_nonneg {ι : Type*} (s : finset ι) (a : ι → ℝ) :
0 ≤ (∑ i in s, (a i)^2) :=
begin
classical,
apply finset.induction_on s ,
{simp,},
rintros j s h1 h2,
have h3 : 0 ≤ ((a j)^2),
{exact pow_two_nonneg (a j),},
--have h:=finset.sum_insert h1,
end
```

I wanted to use finset.sum_insert h1 to close the goal, but `have h:=finset.sum_insert h1`

gives me four new goals.

What can I do next to solve the goal?

#### Eric Rodriguez (May 27 2021 at 10:00):

just `rw`

it; `have`

is confused about some of the implicit arguments, which could be anything. if you `rw`

, it'll be unified with what's in the goal, and then `linarith`

should probably finish it

#### Alex Zhang (May 27 2021 at 10:06):

Cool! The goal is sovled. What `have`

gave me confused me at the beginning...

#### Alex Zhang (May 27 2021 at 10:08):

Could you explain why I need to use `classical`

at the beginning?

#### Eric Rodriguez (May 27 2021 at 10:16):

`classical`

makes all propositions "have an answer"/be *decidable*; to us mathematicians, this is self-evident, but as Lean is designed as a programming language it isn't obvious *what* the decision procedure is, which it needs to "decide" it

#### Eric Rodriguez (May 27 2021 at 10:16):

in this case, the induction needs a `[decidable_eq ι]`

argument, which you could've used instead

Last updated: Dec 20 2023 at 11:08 UTC