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